Software Model Checking
Sagar Chaki, Alex Groce, Ofer Strichman,
Explaining
Abstract Counterexamples,
12th
International Symposium on Foundations of Software Engineering (FSE)
2004
PDF
S. Chaki, E. M. Clarke, J. Ouaknine, N. Sharygina,
Automated,
compositional and iterative deadlock detection,
Proceedings
of MEMOCODE
2004, OMNI Press.
PDF
D. Kroening, S. Seshia, J. Ouaknine, O. Strichman,
Abstraction-based
satisfiability solving of Presburger arithmetic,
Proceedings
of CAV 2004,
LNCS.
PDF
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.]
PDF
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.
PS
E. M. Clarke, D. Kroening, J. Ouaknine, O. Strichman,
Completeness
and
complexity of bounded model checking,
Proceedings of VMCAI
2004, LNCS
2937
PS
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
PS
Flavio Lerda, Nishant Sinha, Michael Theobald,
Symbolic
Model Checking of Software. 2nd
Workshop on Software Model Checking
(SoftMC) 2003
PS
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
PS
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
PDF
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)
PS
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
PDF
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
PDF
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.
ABS
PS
PDF
PPT
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.
ABS
PS
PDF
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.)
ABS
PS
PDF
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
ABS
PS
PDF
Immerman, N., Rabinovich, A., Reps, T., Sagiv, M., and Yorsh, G.,
Verification via structure simulation.
Proc. Int.
Conf. on Computer-Aided Verification, 2004.
ABS
PS
PDF
Reps, T., Sagiv, M., and Yorsh, G.,
Symbolic implementation of the best transformer.
Proc. Verification, Model Checking, and Abstract
Interpretation, 2004.
ABS
PS
PDF
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
ABS
PS
PDF
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
ABS
PS
PDF
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
ABS
PS
PDF
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.
ABS
PS
PDF
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.
ABS
PS
PDF
PPT
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.
ABS
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.
ABS
PS
PDF
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.