| |||||||||||
| |||||||||||
|
| 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. |
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 | |
| 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 | |
| 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. | ABS | PS | 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 | ||
| 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 | ||
|
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 | ||
|
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 | ||
|
Reps, T., Sagiv, M., and Yorsh, G.,
Symbolic implementation of the best transformer.
Proc. Verification, Model Checking, and Abstract Interpretation, 2004. |
ABS | PS | ||
| 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 | ||
| 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 | ||
| 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 | ||
| 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 | ||
| 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 | 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 | ||
| 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. | |