CMU logo Wisconsin logo
Software Model Checking
Sagar Chaki, Alex Groce, Ofer Strichman, Explaining Abstract Counterexamples, 12th International Symposium on Foundations of Software Engineering (FSE) 2004
S. Chaki, E. M. Clarke, J. Ouaknine, N. Sharygina, Automated,
compositional and iterative deadlock detection
, Proceedings of MEMOCODE
2004, OMNI Press.
D. Kroening, S. Seshia, J. Ouaknine, O. Strichman, Abstraction-based
satisfiability solving of Presburger arithmetic
, Proceedings of CAV 2004,
LNCS.
S. Chaki, E. M. Clarke, J. Ouaknine, N. Sharygina, N. Sinha,
State/event-based software model checking, Proceedings of IFM 2004, LNCS
2999
. [Runner-up for BCS-FACS Best Paper Award.]
S. Chaki, E. M. Clarke, A. Groce, J. Ouaknine, O. Strichman, K. Yorav,
Efficient verification of sequential and concurrent C programs, Formal
Methods in System Design, 2004.
E. M. Clarke, D. Kroening, J. Ouaknine, O. Strichman, Completeness and
complexity of bounded model checking
, Proceedings of VMCAI 2004, LNCS
2937
Sagar Chaki, Edmund Clarke, Alex Groce, Ofer Strichman, Predicate Abstraction with Minimum Predicates. 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME) 2003
Flavio Lerda, Nishant Sinha, Michael Theobald, Symbolic Model Checking of Software. 2nd Workshop on Software Model Checking (SoftMC) 2003
Sagar Chaki, Joel Ouaknine, Karen Yorav, Edmund Clarke, Automated Compositional Abstraction Refinement for Concurrent C Programs: A Two-Level Approach, 2nd Workshop on Software Model Checking (SoftMC) 2003
E. M. Clarke, D. Kroening, N. Sharygina, K. Yorav, Predicate Abstraction of ANSI-C Programs using SAT, Proc. of the Model Checking for Dependable Software-Intensive Systems Workshop (DSN) 2003
S. Chaki, E.M. Clarke, A. Groce, S. Jha, H. Veith, Modular Verification of Software Components in C, 25th International Conference on Software Engineering (ICSE) 2003: 385-395 (Distinguished Paper Award)
This work involves collaboration with members of the research group supported by other funding sources.
Verification of Hybrid Systems
E.M. Clarke, A Fehnker, Zhi Han, B. Krogh, J. Ouaknine, O. Stursberg, M. Theobald. Abstraction and Counterexample-guided Refinement of Hybrid Systems. To appear in International Journal of Foundations of Computer Science, (IJFCS) 2003
Edmund M. Clarke, Ansgar Fehnker, Zhi Han, Bruce H. Krogh, Olaf Stursberg, Michael Theobald. Verification of Hybrid Systems Based on Counterexample-Guided Abstraction Refinement. Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference (TACAS) 2003: 192-207
This work involves collaboration with members of the research group supported by other funding sources.
Authorization
Jha, S. and Reps, T., Analysis of SPKI/SDSI certificates using model checking. To appear in Journal of Computer Security.
S. Schwoon, S. Jha, T. Reps, and S. Stubblebine, On generalized authorization problems. Proc. 16th IEEE Computer Security Foundations Workshop, (June 30 - July 2, 2003, Asilomar, Pacific Grove, CA), pp. 202-218.
Jha, S. and Reps, T., Analysis of SPKI/SDSI certificates using model checking. In Proc. 15th IEEE Computer Security Foundations Workshop, (Cape Breton, Nova Scotia, June 24-26, 2002), pp. 129-146.
Static Analysis of Software
Reps, T., Sagiv, M., and Wilhelm, R., Static program analysis via 3-valued logic. Proc. Int. Conf. on Computer-Aided Verification, 2004.
(Invited paper.)
Jeannet, B., Loginov, A., Reps, T., and Sagiv, M.,
A relational approach to interprocedural shape analysis.
Proc. 11th Int. Static Analysis Symp., Lecture Notes in Computer Science, Springer-Verlag, New York, NY, 2004. (c) Springer-Verlag
Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., and Yorsh, G.,
Verification via structure simulation. Proc. Int. Conf. on Computer-Aided Verification, 2004.
Reps, T., Sagiv, M., and Yorsh, G., Symbolic implementation of the best transformer. Proc. Verification, Model Checking, and Abstract
Interpretation
, 2004.
Yorsh, G., Reps, T., and Sagiv, M., Symbolically computing most-precise abstract operations for shape analysis. In Proc. TACAS, Springer-Verlag, New York, NY, 2004. (c) Springer-Verlag
Reps, T., Sagiv, M., and Loginov, A., Finite differencing of logical formulas for static analysis. Proc. European Symp. on Programming, Lecture Notes in Computer Science, Vol. 2618, Springer-Verlag, New York, NY, 2003, pp. 380-398. (c) Springer-Verlag
Yahav, E., Reps, T., Sagiv, M., and Wilhelm, R. Verifying temporal heap properties specified via evolution logic. Proc. European Symp. on Programming, Lecture Notes in Computer Science, Vol. 2618, Springer-Verlag, New York, NY, 2003, pp. 204-222. (c) Springer-Verlag
Reps, T., Loginov, A., and Sagiv, M., Semantic minimization of 3-valued propositional formulae. Proc. IEEE Symp. on Logic in Computer Science, (Copenhagen, Denmark, July 22-25, 2002), pp. 40-54.
Sagiv, M., Reps, T., and Wilhelm, R., Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems 24, 3 (2002), 217-298.
Yorsh, G., Reps, T., Sagiv, M., and Wilhelm, R., Logical characterizations of heap abstractions. Submitted for journal publication.
Other
Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., and Yorsh, G., The boundary between decidability and undecidability for transitive closure logics. To appear in Proc. Computer Science Logic, 2004.
Alur, R., Benedikt, M., Etessami, K., Godefroid, P., Reps, T., and
Yannakakis, M., Analysis of recursive state machines.
ACM Trans. on Program. Lang. and Syst., to appear.
Gopan, D., DiMaio, F., Dor, N., Reps, T., and Sagiv, M., Numeric domains with summarized dimensions. In Proc. TACAS, Springer-Verlag, New York, NY, 2004.
 
Book Chapters
Reps, T., Sagiv, M., and Wilhelm, R., Shape analysis and applications. The Compiler Design Handbook: Optimizations and Machine Code Generation, CRC Press, 2002, 175-217.
 

     Please send any comments or suggestions about this website to Nishant Sinha or Stephen Magill.