Formal Methods

1. Kwon, YoungMin, Gul Agha. "LTLC: Linear Temporal Logic for Control," 11th International Conference on Hybrid Systems: Computation and Control (HSCC) (to appear), 2008. [pdf] [bib]
2. Donkervoet, Bill, Gul Agha. "Reflecting on Adaptive Distributed Monitoring," Formal Methods for Components and Objects, 2007. [pdf] [bib]
3. Rosu, Grigore, Koushik Sen. "An Instrumentation Technique for Online Analysis of Multithreaded Programs," Special Issue of Concurrency and Computation: Practice and Experience (CC:PE), 2006. [pdf] [ps] [bib]
4. Sen, Koushik, Mahesh Viswanathan, Gul Agha. "Model-Checking Markov Chains in the presence of Uncertainties," TACAS, 2006. [pdf] [ps] [bib]
5. Vardhan, Abhay. "Learning To Verify Systems," Ph.D. Thesis, Dept. of Computer Science, 2006. [pdf] [bib]
6. Kwon, YoungMin. "Probabilistic Modeling and Verification of Large Scale Systems," Technical Report, UIUCDCS-R-2006-2687, Department of Computer Science, University of Illinois at Urbana Champaign, 2006. [pdf] [ps] [bib]
7. Sen, Koushik, Gul Agha. "Automated Systematic Testing of Open Distributed Programs," FASE, 2006. [pdf] [ps] [bib]
8. Sen, Koushik, Gul Agha. "CUTE and jCUTE : Concolic Unit Testing and Explicit Path Model-Checking Tools," CAV. Tool Paper, 2006. [pdf] [ps] [bib]
9. Sen, Koushik, Mahesh Viswanathan. "Model Checking Multithreaded Programs with Asynchronous Atomic Methods," CAV, 2006. [pdf] [ps] [bib]
10. Sen, Koushik. "Scalable Automated Methods for Dynamic Program Analysis," PhD Dissertation, 2006. [pdf] [ps] [bib]
11. Sen, Koushik, Abhay Vardhan, Gul Agha, Grigore Rosu. "Efficient Decentralized Monitoring of Safety in Distributed Systems," Submitted to ACM TOSEM [invited], 2006. [pdf] [ps] [bib]
12. Sen, Koushik, Grigore Rosu, Gul Agha. "Online Efficient Predictive Safety Analysis of Multithreaded Programs," International Journal on Software Technology and Tools Transfer (STTT) (To Appear), 2005. [pdf] [ps] [bib]
13. Agha, Gul, Jose Meseguer, Koushik Sen. "PMaude: Rewrite-based Specification Language for Probabilistic Object Systems," Electronic Notes in Theoretical Computer Science, Elsevier Science, 2005. Expanded version of the paper that appeared in Proceedings of the 3rd Workshop on Quantitative Aspects of Programming Languages (To Appear)., 2005. [bib]
14. Escobar, Santiago, Jose Meseguer, Prasanna Thati. "Natural Narrowing for General Term Rewriting Systems," International Conference on Term Rewriting Techniques and Applications, 2005. [pdf] [ps] [bib]
15. Meseguer, Jose, Prasanna Thati. "Symbolic Reachability Analysis Using Narrowing and its Application to Verification of Cryptographic Protocols," to appear in Journal of Higher Order and Symbolic Computation , 2005. [pdf] [ps] [bib]
16. Sen, Koushik, Mahesh Viswanathan, Gul Agha. "On Statistical Model Checking of Stochastic Systems," In 17th International Conference on Computer Aided Verification, (CAV'05), LNCS (To Appear), 2005. [pdf] [pdf] [ps] [ps] [bib]
17. Agha, Gul, Jose Meseguer, Koushik Sen. "PMaude: Rewrite-based Specification Language for Probabilistic Object Systems," 3rd Workshop on Quantitative Aspects of Programming Languages (QAPL 05), 2005. [bib]
18. Vardhan, Abhay, Koushik Sen, Mahesh Viswanathan, Gul Agha. "Using Language Inference to Verify omega-regular Properties," In Proceedings of 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005), LNCS, 2005. [pdf] [ps] [bib]
19. Agha, Gul, Carl Gunter, Michael Greenwald, Sanjeev Khanna, Jose Meseguer, Koushik Sen, Prasanna Thati. "Formal Modeling and Analysis of DoS Using Probabilistic Rewrite Theories," Foundations of Computer Security (FCS), 2005. [bib]
20. Sen, Koushik, Grigore Rosu, Gul Agha. "Detecting Errors in Multithreaded Programs by Generalized Predictive Analysis of Executions," FMOODS, 2005. [pdf] [ps] [bib]
21. Godefroid, Patrice, Nils Klarlund, Koushik Sen. "DART: Directed Automated Random Testing," PLDI, 2005. [pdf] [ps] [bib]
22. Thati, Prasanna, Jose Meseguer. "Complete Symbolic Reachability Analysis Using Back-and-Forth Narrowing," International Conference on Algebra and Coalgebra in Computer Science, to appear, 2005. [bib]
23. Sen, Koushik, Mahesh Viswanathan, Gul Agha. "VESTA: A Statistical Model Checker and Analyzer for Probabilistic Systems," In 2nd International Conference on the Quantitative Evaluation of Systems, IEEE, (Tool paper), 2005. [pdf] [ps] [bib]
24. Artho, Cyrille, Howard Barringer, Allen Goldberg, Klaus Havelund, Sarfraz Khurshid, Michael Lowry, Corina Pasareanu, Grigore Rosu, Koushik Sen, Willem Visser, Rich Washington. "Combining Test Case Generation and Runtime Verification," Theoretical Computer Science (TCS), 2005. [pdf] [ps] [bib]
25. Kwon, YoungMin, Gul Agha. "iLTLChecker: A Probabilistic Model Checker for Multiple DTMCs," 2nd International Conference on the Quantitative Evaluation of Systems, IEEE, (Tool paper), 2005. [pdf] [ps] [bib]
26. Vardhan, Abhay, Mahesh Viswanathan. "Learning to Verify Branching Time Properties," Techincal Report UIUCDCS-R-2004-2445, UILU-ENG-2004-1747 (this is a long version of a paper to appear at the 20th IEEE/ACM International Conference on Automated Software Engineering, Long Beach, California, USA), 2005. [pdf] [bib]
27. Sen, Koushik, Mahesh Viswanathan, Gul Agha. "Statistical Model Checking of Black-Box Probabilistic Systems," In 16th conference on Computer Aided Verification (CAV'04), volume 3114 of Lecture Notes in Computer Science, pages 202-215, Boston, MA, USA, July 2004. Springer., 2004. [pdf] [ps] [bib]
28. Rosu, Grigore, Koushik Sen. "An Instrumentation Technique for Online Analysis of Multithreaded Programs," In Workshop on Parallel and Distributed Systems: Testing and Debugging (PADTAD'04) (Satellite workshop of IPDPS'04), Santa Fe, New Mexico, USA, April 2004. IEEE digital library. Invited Paper., 2004. [pdf] [ps] [bib]
29. Sen, Koushik, Grigore Rosu, Gul Agha. "Online Efficient Predictive Safety Analysis of Multithreaded Programs," In Proceedings of 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'04), volume 2988 of Lecture Notes in Computer Science, pages 123-138, Barcelona, Spain, March 2004., 2004. [pdf] [ps] [bib]
30. Vardhan, Abhay, Koushik Sen, Mahesh Viswanathan, Gul Agha. "Learning to Verify Safety Properties," In 6th International Conference on Formal Engineering Methods (ICFEM'04), Seattle, WA, USA, November 2004, LNCS 3308, pages 274-288, Copyright Springer-Verlag (http://www.springer.de/comp/lncs/index.html), 2004. [pdf] [ps] [bib]
31. Sen, Koushik, Abhay Vardhan, Gul Agha, Grigore Rosu. "On Specifying and Monitoring Epistemic Properties of Distributed Systems," In 2nd International Workshop on Dynamic Analysis (WODA'04), Satellite workshop of ICSE 2004, pages 32-35. British Institution of Electrical Engineers (IEE), May 2004., 2004. [pdf] [ps] [bib]
32. Naldurg, Prasad, Koushik Sen, Prasanna Thati. "A Temporal Logic Based Approach to Intrusion Detection," In 24th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems (FORTE'04), volume 3235 of Lecture Notes in Computer Science, pages 359-376, Madrid, Spain, September 2004. Springer., 2004. [pdf] [ps] [bib]
33. Thati, Prasanna, Carolyn Talcott, Gul Agha. "Techniques for Executing and Reasoning About Specification Diagrams," International Conference on Algebraic Methodology and Software Technology (AMAST), 2004. [pdf] [ps] [bib]
34. Thati, Prasanna, Grigore Rosu. "Monitoring Algorithms for Metric Temporal Logic Specifications," Runtime Verification (RV), 2004. [pdf] [ps] [bib]
35. Thati, Prasanna, Mahesh Viswanathan. "Verification of Asynchronous Systems with Unbounded and Unordered Message Buffers," International Workshop on Automated Verification of Infinite State Systems (AVIS), 2004. [pdf] [ps] [bib]
36. Escobar, Santiago, Jose Meseguer, Prasanna Thati. "Natural Rewriting for General Term Rewriting Systems," Submitted to International Symposium on Logic Based Program Synthesis and Tranformation (LOPSTR), 2004. [pdf] [ps] [bib]
37. Vardhan, Abhay, Koushik Sen, Mahesh Viswanathan, Gul Agha. "Actively Learning to Verify Safety for FIFO Automata," In 24th Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'04), Lecture Notes in Computer Science, Chennai, India, December, LNCS 3328, pages 494-505, Copyright Springer-Verlag (http://www.springer.de/comp/lncs/index.html), 2004. [pdf] [ps] [bib]
38. Barringer, Howard, Allen Goldberg, Klaus Havelund, Koushik Sen. "Rule-Based Runtime Verification," In Proceedings of 5th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'04), volume 2937 of Lecture Notes in Computer Science, pages 44-57, Venice, Italy, January 2004. Springer., 2004. [pdf] [ps] [bib]
39. Sen, Koushik, Mahesh Viswanathan, Gul Agha. "Learning Continuous Time Markov Chains from Sample Executions," In 1st International Conference on Quantitative Evaluation of Systems (QEST'04), pages 146-155, Enschede, The Netherlands, September 2004. IEEE., 2004. [pdf] [ps] [bib]
40. Kwon, YoungMin, Gul Agha. "Linear Inequality LTL (iLTL): A Model Checker for Discrete Time Markov Chains," International Conference on Formal Engineering Methods (ICFEM), 2004. [pdf] [ps] [bib]
41. Sen, Koushik, Abhay Vardhan, Gul Agha, Grigore Rosu. "Efficient Decentralized Monitoring of Safety in Distributed Systems," In Proceedings of 26th International Conference on Software Engineering (ICSE'04), pages 418-427, Edinburgh, UK, May 2004. IEEE., 2004. [pdf] [ps] [bib]
42. Barringer, Howard, Allen Goldberg, Klaus Havelund, Koushik Sen. "Program Monitoring with LTL in Eagle," In Workshop on Parallel and Distributed Systems: Testing and Debugging (PADTAD'04) (Satellite workshop of IPDPS'04), Santa Fe, New Mexico, USA, April 2004. IEEE digital library., 2004. [pdf] [ps] [bib]
43. Sen, Koushik, Grigore Rosu, Gul Agha. "Runtime Safety Analysis of Multithreaded Programs," 9th European Software Engineering Conference and 11th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (ESEC/FSE'03), pages 337{346, Helsinki, Finland, September, 2003. ACM., 2003. [pdf] [ps] [bib]
44. Kumar, Nirman, Koushik Sen, Jose Meseguer, Gul Agha. "A Rewriting Based Model for Probabilistic Distributed Object Systems," In Proceedings of 6th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS'03), volume 2884 of Lecture Notes in Computer Science, pages 32{46, Paris, France, November 2003. Springer., 2003. [pdf] [ps] [bib]
45. Thati, Prasanna. "A theory of testing for asynchronous concurrent systems," Phd Dissertation, University of Illinois at Urbana Champaign, October, 2003. [pdf] [ps] [bib]
46. Sen, Koushik, Grigore Rosu, Gul Agha. "Generating Optimal Linear Temporal Logic Monitors by Coinduction," In Proceedings of 8th Asian Computing Science Conference (ASIAN'03), volume 2896 of Lecture Notes in Computer Science, pages 260{75, Mumbai, India, December 2003. Springer., 2003. [pdf] [ps] [bib]
47. Sen, Koushik. "Predictive Safety Analysis of Concurrent Programs," Master's thesis, Supervisor Gul Agha, University of Illinois at Urbana-Champaign, May, 2003. [pdf] [ps] [bib]
48. Sen, Koushik, Grigore Rosu. "Generating Optimal Monitors for Extended Regular Expressions," In Proceedings of the 3rd Workshop on Runtime Verification (RV'03), volume 89(2) of Electronic Notes in Theoretical Computer Science, Boulder, Colorado, USA, July 2003. Elsevier Science., 2003. [pdf] [ps] [bib]
49. Thati, Prasanna, Koushik Sen, Narciso Marti-Oliet. "An Executable Specification of Asynchronous Pi-Calculus and May-Testing in Maude 2.0," WRLA (ENTCS), 2002. [pdf] [ps] [bib]
50. Thati, Prasanna, Reza Ziaei, Gul Agha. "Theory of May Testing for Asynchronous Calculi with Locality and No Name Matching," International Conference on Algebraic Methodology and Software Technology (AMAST), 2002. [pdf] [ps] [bib]
51. Ziaei, Reza, Gul Agha, Prasanna Thati. "A Theory of May Testing for Actors," International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS), 2002. [pdf] [ps] [bib]
52. Sen, Koushik, Gul Agha. "Thin Middleware for Ubiquitous Computing," Process Coordination and Ubiquitous Computing, CRC Press, 2002. [pdf] [ps] [bib]
53. Thati, Prasanna, Po-Hao Chang, Gul Agha. "Crawlets: Agents for high performance web search engines," IEEE International Conference on Mobile Agents (MA), 2001. [ps] [bib]
54. Thati, Prasanna. "Towards an Algebriac Formulation of Actors," Masters Thesis, 2001. [pdf] [ps] [bib]
55. Agha, Gul, Prasanna Thati. "Actors: A model for reasoning about open distributed systems," in H. Bowman and J. Derrick (editors), Formal Methods for Distributed Processing - An Object Oriented Approach, Chap. 8, Cambridge University Press, 2001. [pdf] [ps] [bib]
56. Agha, Gul, Prasanna Thati, Reza Razavi. "Actors: A Model for Reasoning about Open Distributed Systems," Formal methods for distributed processing: a survey of object-oriented approaches, 2001. [bib] [pdf]
57. Agha, Gul. "Abstracting Interaction Patterns: A Programming Paradigm for Open Distributed Systems," in Elie Najm and Jean-Bernard Stefani (editors), Formal Methods for Open Object-Based Distributed Systems, pp 135-153, Chapman and Hall (on behalf of the International Federation for Information Processing), 1997. [pdf] [ps] [bib]
58. Agha, Gul, Ian A. Mason, Scott Smith, Carolyn Talcott. "A Foundation for Actor Computation," Journal of Functional Programming, Vol. 7 pp 1-72, 1997. [pdf] [ps] [bib]
59. Agha, Gul. "Formal Methods for Actors: A Progress Report," Formal Description Techniques V, IFIP Transactions, vol. C-10, pp 217-228, Elsevier-North Holland, 1993. [bib]
60. Agha, Gul, Ian A. Mason, Scott Smith, Carolyn Talcott. "Towards a Theory of Actor Computation," The Third International Conference on Concurrency Theory (CONCUR '92), Stony Brook, NY, Lecture Notes in Computer Science No. 630, pp 565-579, Springer Verlag, August, 1992. [pdf] [ps] [bib]