Selected publications of the STeP Research Group

Selected Publications of the STeP research group (by topic)
(View by year of publication)

Static Analysis

Sriram Sankaranarayanan, Henny B. Sipma, Zohar Manna, Fixed point iteration for computing the time elapse operator, In Proc. Hybrid Systems: Computation and Control (HSCC 2006), Lecture Notes in Computer Science. Vol. 3927, Springer Verlag, 2006.
Sriram Sankaranarayanan, Michael A. Colon, Henny B. Sipma, Zohar Manna, Efficient Strongly Relational Polyhedral Analysis, In Proc. Verification, Model Checking, and Abstract Interpretation (VMCAI 2006), Lecture Notes in Computer Science, Vol. 3855, Springer Verlag, 2006.
Sriram Sankaranarayanan, Mathematical Analysis of Programs, PhD Thesis, Stanford University, 2005.
Aaron R. Bradley, Zohar Manna, Henny B. Sipma, Termination Analysis of Integer Linear Loops, In Proc. of the 16th International Conference on Concurrency Theory (CONCUR'05), San Francisco, August 2005, Springer Verlag, LNCS 3653, pp 488-502.
Aaron R. Bradley, Zohar Manna, Henny B. Sipma, Linear Ranking with Reachability, In Proc. of 17th International Conference on Computer Aided Verification (CAV'05), Springer Verlag, 2005, LNCS 3576, pp 491-504.
Aaron R. Bradley, Zohar Manna, Henny B. Sipma, The Polyranking Principle, In Proc. 32nd International Colloquium on Automata, Languages and Programming (ICALP 2005), Lisboa, Portugal, July 2005, Springer Verlag, LNCS 3580, pp 1349-1361.
Aaron R. Bradley, Zohar Manna, Henny B. Sipma, Termination of Polynomial Programs, In Proc. of Verification, Model Checking and Abstract Interpretation (VMCAI'05), LNCS 3385, Springer Verlag, 2005.
Sriram Sankaranarayanan, Henny B. Sipma, Zohar Manna, Scalable Analysis of Linear Systems using Mathematical Programming, In Proc.of Verification, Model Checking and Abstract Interpretation (VMCAI'05), LNCS 3385, pp 21-47, Springer Verlag, 2005.
Sriram Sankaranarayanan, Henny B. Sipma, Zohar Manna, Constraint-Based Linear-Relations Analysis, In Static Analysis Symposium (SAS'04), LNCS 3148 Springer Verlag, pp 53-68 .
Sriram Sankaranarayanan, Henny B. Sipma, Zohar Manna, Constructing Invariants for Hybrid systems. In Hybrid Systems: Computation and Control (HSCC 2004).
Sriram Sankaranarayanan, Henny B. Sipma, Zohar Manna, Non-Linear Loop Invariant Generation, In Principles of Programming Languages (POPL 2004).
Sriram Sankaranarayanan, Henny Sipma, Zohar Manna, Petri Net Analysis Using Invariant Generation. In Verification: Theory and Practice, vol. 2772 of Lecture Notes in Computer Science, 2003.
Michael A. Colon, Deductive Techniques for Program Analysis, PhD Thesis, Stanford University, 2003.
Michael A. Colon, Sriram Sankaranarayanan, Henny B. Sipma. Linear Invariant Generation using Non-linear Constraint Solving. In Computer Aided Verification (CAV 2003), vol. 2725 of Lecture Notes in Computer Science, Springer Verlag, pp. 420-433, 2003.
Michael Colon and Henny Sipma. Practical Methods for Proving Program Termination. In 14th International Conference on Computer Aided Verification (CAV), LNCS 2404, Springer-Verlag, pp 442-454, 2002.
Michael Colon, Henny Sipma. Synthesis of Linear Ranking Functions. In 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS 2031, Springer-Verlag, pp 67-81, 2001.
Michael Colon and Tomas Uribe, Generating Finite-State Abstractions of Reactive Systems Using Decision Procedures. In International Conference on Computer-Aided Verification, CAV'98, pp. 293-304, vol. 1427 of LNCS, Springer-Verlag, June/July 1998.
Tomas Uribe. Abstraction-based Deductive-Algorithmic Verification of Reactive Systems. PhD Thesis. Appeared as Technical Report STAN-CS-TR-99-1618, Stanford University.
Nikolaj Bjørner, I. Anca Browne and Zohar Manna. Automatic Generation of Invariants and Intermediate Assertions. Theoretical Computer Science, vol. 173(1), pp. 49-87, February 1997. Original version appeared in 1st International Conference on Principles and Practice of Constraint Programming, Lecture Notes in Computer Science 976, Cassis, France, pp. 589-623, September 1995.

Decision Procedures

Ting Zhang, Henny B. Sipma, Zohar Manna, Decision procedures for term algebras with integer constraints, In Information and Computation, volume 204, pp 1526-1574, October 2006.
Aaron R. Bradley, Zohar Manna, Henny B. Sipma, What's decidable about Arrays?, In Proc. Verification, Model Checking, and Abstract Interpretation (VMCAI 2006), Lecture Notes in Computer Science, Vol. 3855, Springer Verlag, 2006.
Ting Zhang, Henny B. Sipma, Zohar Manna, Decision Procedures for Queues with Integer Constraints, In Proc. Foundations of Software Technology and Theoretical Computer Science (FSTTCS), December 2005, Lecture Notes in Computer Science, Volume 3821, Springer-Verlag.
Ting Zhang, Henny B. Sipma, Zohar Manna, The Decidability of the First-order Theory of Knuth-Bendix Order, To appear in CADE'05.
Ting Zhang, Henny B. Sipma, and Zohar Manna, Term algebras with length function and bounded quantifier alternation. In 17th Internation Conference on Theorem Proving in Higher Order Logics (TPHOLS'04), LNCS 3223, pp 321-336, Springer Verlag 2004.
Ting Zhang, Henny B. Sipma, and Zohar Manna, Decision procedures for recursive data structures with integer constraints. In International Joint Conference on Automated Reasoning (IJCAR'04), LNCS 3097, Springer Verlag, pp 152-167, 2004.
Calogero G. Zarba, The Combination Problem in Automated Reasoning. PhD thesis, Stanford University, 2004.
Calogero G. Zarba, Combining Sets with Elements, In Verification: Theory and Practice, vol. 2772 of Lecture Notes in Computer Science, 2004.
Zohar Manna and Calogero Zarba, Combining decision procedures. In Formal Methods at the Crossroads: from Panacea to Foundational Support, Vol 2787 of Lecture Notes in Computer Science, pp 381-422, 2003.
Calogero G. Zarba, Zohar Manna, Henny Sipma, Combining Theories Sharing Dense Orders. In Automated Reasoning with Analytic Tableaux and Related Methods: Position Papers and Tutorials Marta Cialdea Mayer and Fiora Pirri, editors. Technical Report
Calogero G. Zarba. A tableau calculus for combining non-disjoint theories. To appear in TABLEAUX'02. RT-DIA-80-2003, pages 83-98, Università di Roma Tre. Aracne Editrice, 2003
Calogero G. Zarba. A tableau calculus for combining non-disjoint theories. In TABLEAUX'02, 2002.
Calogero G. Zarba. Combining Multisets with Integers. In CADE'02, 2002.
Calogero G. Zarba. Combining Sets with Integers, In Alessandro Armando, editor, Frontiers of Combining Systems (FROCOS 2002), Lecture Notes in Artificial Intelligence, Springer Verlag, 2002.
Calogero G. Zarba. Combining Non-Disjoint Theories. In Rajeev Gorè, Alexander Leitsch, and Tobias Nipkow, editors, International Joint Conference on Automated Reasoning. Short Papers (IJCAR 2001), Technical Report DII 11/01, pages 180-189. University of Siena, Italy, 2001.
Calogero G. Zarba. Combining Lists with Integers . In Rajeev Gorè, Alexander Leitsch, and Tobias Nipkow, editors, International Joint Conference on Automated Reasoning. Short Papers (IJCAR 2001), Technical Report DII 11/01, pages 170-179. University of Siena, Italy, 2001.
Nikolaj Bjorner. Integrating Decision Procedures for Temporal Verification. PhD Thesis, Stanford University, 1998.
Nikolaj Bjørner, Mark Stickel and Tomás E. Uribe. A Practical Integration of First-Order Reasoning and Decision Procedures, Proceedings of the 14th Intl. Conf. on Automated Deduction, LNCS vol 1249, Springer-Verlag, pp 101--115, 1997.

Runtime Verification

Ben d'Angelo, Sriram Sankaranarayanan, Cesar Sanchez, Will Robinson, Bernd Finkbeiner, Henny B. Sipma, Sandeep Mehrotra, Zohar Manna, LOLA: Runtime Monitoring of Synchronous Systems, In Proc. of the 12th International Symposium of Temporal Representation and Reasoning (TIME 2005), pp. 166-174, IEEE Computer Society Press, 2005.
Bernd Finkbeiner, Sriram Sankaranarayanan, and Henny B. Sipma, Collecting statistics about runtime executions. In Formal Methods in System Design, Vol. 27, pp 253-274, November 2005.
Bernd Finkbeiner and Henny B. Sipma, Checking Finite Traces Using Alternating Automata. In Formal Methods in System Design, vol 24, pages 101-127, 2004.
Bernd Finkbeiner, Sriram Sankaranarayanan and Henny Sipma. Collecting Statistics over Runtime Executions. In RV'02, 2002.
Bernd Finkbeiner and Henny Sipma. Checking Finite Traces using Alternating Automata. Workshop on Runtime Verification, CAV'01, 2001.

Event Correlation and Middleware Formalization

Cesar Sanchez, Henny B. Sipma, Christopher D. Gill, and Zohar Manna, Distributed Priority Inheritance for Real-Time and Embedded Systems. To appear in OPODIS'06.
Venkita Subramonian, Christopher Gill, Cesar Sanchez, and Henny B. Sipma, Reusable Models for Timing and Liveness Analysis of Middleware for Distributed Real-Time and Embedded Systems. To appear in EMSOFT'06.
Cesar Sanchez, Henny B. Sipma, Zohar Manna, Christopher D. Gill, Efficient Distributed Deadlock Avoidance with Liveness Guarantees. To appear in EMSOFT'06.
Cesar Sanchez, Henny B. Sipma, Zohar Manna, Venkita Subramonian, and Christopher D. Gill, On Efficient Distributed Deadlock Avoidance for Distributed Real-Time and Embedded Systems, In Proc. of the 20th IEEE Int'l Parallel and Distributed Processing Symposium (IPDPS'06), IEEE Computer Society Press, 2006.
Cesar Sanchez, Henny B. Sipma, Venkita Subramonian, Christopher Gill, Zohar Manna, Thread Allocation Protocols for Distributed Real-Time and Embedded Systems. In Formal Techniques for Networked and Distributed Systems (FORTE 2005): 25th IFIP WG 6.1 International Conference, October 2005, Lecture Notes in Computer Science, Volume 3731, Springer Verlag, pp 159-173.
Cesar Sanchez, Matteo Slanina, Henny B. Sipma, Zohar Manna, Expressive Completeness of an Event-Pattern Reactive Programming Language. In Formal Techniques for Networked and Distributed Systems (FORTE 2005): 25th IFIP WG 6.1 International Conference, October 2005, Lecture Notes in Computer Science, Volume 3731, Springer Verlag, pp 529-532.
Cesar Sanchez, Henny B. Sipma, Matteo Slanina, Zohar Manna, Final Semantics for Event-Pattern Reactive Programs, In Proc. of the First Conference on Algebra and Coalgebra in Computer Science (CALCO'05), Swansea, UK, September 2005, Springer Verlag, LNCS 3629, pp 364-378.
Cesar Sanchez, Sriram Sankaranarayanan, Henny Sipma, Ting Zhang, David Dill, and Zohar Manna, Event Correlation: Language and Semantics, In Embedded Software (EMSOFT), vol 2855 of Lecture Notes in Computer Science, Springer Verlag, pp 323-339.

Controlled Systems and Synthesis

Matteo Slanina, Henny B. Sipma, and Zohar Manna, Proving ATL* Properties of Infinite-State Systems. To appear in ICTAC'06.
Matteo Slanina. Control Rules for Reactive System Games. 2002 AAAI Spring Symposium on Logic-Based Program Synthesis.

Anuchit Anuchitanukul, Synthesis of Reactive Programs, PhD Thesis, Stanford University, September 1995.
Zohar Manna and Henny Sipma. A Deductive Approach towards Controller Synthesis. In 1995 IEEE International Symposium on Intelligent Control, Monterey, CA, 1995, pp. 35--41.
Anuchit Anuchitanukul and Zohar Manna, Realizability and Synthesis of Reactive Modules, In Computer Aided Verification (CAV'94), LNCS 818, Springer Verlag, pp 156-169, 1994.
Henny Sipma and Zohar Manna. Specification and Verification of Controlled Systems. In Proceedings of the Third International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems, Lecture notes in Computer Science 863, Springer-Verlag, 1994.

Diagram Verification and Automata

Bernd Finkbeiner, Verification Algorithms based on Alternating Automata, PhD Thesis, Stanford University.
Bernd Finkbeiner. Language Containment Checking with Nondeterministic BDD's. In 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS 2031, Springer-Verlag, pp 24-38, 2001.
Henny Sipma, Tomas Uribe, and Zohar Manna. Model checking and deduction for infinite-state systems . In Logical Perspectives on Language and Information, pp 221-244, CSLI publications, 2001.
Zohar Manna, Henny Sipma, Verification Diagrams: Logic + Automata, In Proceedings of the7th Monterey Workshop: Modelling Software Systems Structures in a Fastly Moving Scenario, pp 226-237, Santa Margherita, 2000.
Zohar Manna, Henny Sipma, Alternating the Temporal Picture for Safety. In Proc. 27th Intl. Colloq. Aut. Lang. Prog.(ICALP). LNCS 1853, Springer-Verlag, pp 429-450, 2000.
Zohar Manna and Henny Sipma, Verification of Parameterized Systems by Dynamic Induction on Diagrams, CAV'99, pp 25-43, LNCS 1633, Springer-Verlag, 1999.
Henny B. Sipma, Tomás E. Uribe and Zohar Manna. Deductive Model Checking. Formal Methods in System Design, Vol 15, pp 49-74 (1999).
Henny Sipma. Diagram-based verification of reactive, real-time, and hybrid systems. PhD Thesis, 1999.
Zohar Manna, Anca Browne, Henny Sipma, and Tomas Uribe. Visual Abstraction for Temporal Verification. In AMAST'98, Vol 1548 of LNCS, pp 28-41, Springer-Verlag, 1998.
Luca de Alfaro, Zohar Manna and Henny B. Sipma. Decomposing, Transforming and Composing Diagrams: The joys of Modular Verification, Technical Report STAN-CS-98-1614, Stanford University, 1998.
Luca de Alfaro, Arjun Kapur and Zohar Manna. Hybrid Diagrams: A Deductive-Algorithmic Approach to Hybrid System Verification. In Proc. of 14th Symposium on Theoretical Aspects of Computer Science, vol. 1200 of Lecture Notes in Computer Science, pp. 153-164, Springer Verlag, Feb. 1997.
Luca de Alfaro, Zohar Manna, Henny B. Sipma and Tomás E. Uribe. Visual Verification of Reactive Systems, in Third International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, Springer-Verlag, 1997.
Henny B. Sipma, Tomás E. Uribe and Zohar Manna. Model Checking and Deduction for Verifying Infinite-state Systems. Logic, Language and Computation, CSLI, 1997.
Henny B. Sipma, Tomás E. Uribe and Zohar Manna. Deductive Model Checking. In 8th International Conference on Computer-Aided Verification, LNCS vol. 1102, pp. 209-219, Springer-Verlag, July 1996.
Luca de Alfaro and Zohar Manna. Temporal Verification by Diagram Transformations. In 8th International Conference on Computer-Aided Verification, LNCS vol. 1102, pp. 287-299, Springer-Verlag, July 1996.
Anca Browne, Luca de Alfaro, Zohar Manna, Henny B. Sipma and Tomás E. Uribe. Diagram-Based Formalisms for the Verification of Reactive Systems, in CADE-13 Workshop on Visual Reasoning, New Brunswick, NJ, July 1996.
I. Anca Browne, Zohar Manna and Henny Sipma. Generalized Temporal Verification Diagrams. In 15th Conference on the Foundations of Software Technology and Theoretical Computer Science, Lecture Notes in Computer Science, Bangalore, India (December 1995).

Real-time and Hybrid Systems

Sriram Sankaranarayanan, Henny B. Sipma, Zohar Manna, Fixed point iteration for computing the time elapse operator, In Proc. Hybrid Systems: Computation and Control (HSCC 2006), Lecture Notes in Computer Science. Vol. 3927, Springer Verlag, 2006.
Sriram Sankaranarayanan, Henny B. Sipma, Zohar Manna, Constructing Invariants for Hybrid systems. In Hybrid Systems: Computation and Control (HSCC 2004).
Nikolaj Bjorner, Zohar Manna, Henny Sipma and Tomás Uribe. Deductive Verification of Real-time Systems using STeP. Theoretical Computer Science, (253) 2001, pp 27-60.
Henny Sipma. Diagram-based verification of reactive, real-time, and hybrid systems. PhD Thesis, 1999.
Zohar Manna and Henny Sipma. Deductive Verification of Hybrid Systems using STeP. In Hybrid Systems: Computation and Control, Lecture Notes in Computer Science 1386, Springer-Verlag, 1998.
Arjun Kapur, Interval and Point-based Approaches to Hybrid Systems Verification, PhD Thesis, Stanford University, August 1997.
Luca de Alfaro, Arjun Kapur and Zohar Manna. Hybrid Diagrams: A Deductive-Algorithmic Approach to Hybrid System Verification. In Proc. of 14th Symposium on Theoretical Aspects of Computer Science, vol. 1200 of Lecture Notes in Computer Science, pp. 153-164, Springer Verlag, Feb. 1997.
Nikolaj Bjørner, Zohar Manna, Henny Sipma and Tomás Uribe. Deductive Verification of Real-time Systems using STeP, 4th International AMAST Workshop on Real-time Systems, LNCS vol 1231, Springer-Verlag, pp 22-43, 1997.
Luca de Alfaro and Zohar Manna, Verification in Continuous Time by Discrete Reasoning, 4th International Conference on Algebraic Methodology and Software Technology (AMAST), Montreal, Canada, pp. 292-306, July 1995.
Arjun Kapur, Thomas A. Henzinger, Zohar Manna and Amir Pnueli. Proving Safety Properties of Hybrid Systems. International Symposium on Formal Techniques in Real Time and Fault Tolerant Systems, Lecture Notes in Computer Science 863, pp. 431-454, Springer-Verlag, 1994.
Edward Chang, Zohar Manna and Amir Pnueli. Compositional Verification of Real-time Systems. In IEEE Symposium on Logic in Computer Science, pp. 458-465, Paris, 1994.

STeP / Verification Case Studies

Nikolaj Bjorner, Zohar Manna, Henny Sipma and Tomás Uribe. Deductive Verification of Real-time Systems using STeP. Theoretical Computer Science, (253) 2001, pp 27-60.
Anca Browne, Henny Sipma, Ting Zhang. Linking STeP with SPIN. In 7th International SPIN Workshop: SPIN Model Checking and Software Verification, LNCS 1885, Springer-Verlag, pp 181-186.
Anca Browne, Bernd Finkbeiner, Zohar Manna, Henny Sipma, The `Cash-Point' Service: A Verification Case Study Using STeP. Formal Aspects of Computing 12 (2000) 4, 218-219
Nikolaj Bjorner, Anca Browne, Michael Colon, Bernd Finkbeiner, Zohar Manna, Henny Sipma, Tomas Uribe. Verifying Temporal Properties of Reactive Systems: A STeP Tutorial. In Formal Methods in System Design, vol 16, pp 227-270.
Zohar Manna, Nikolaj Bjorner, Anca Browne, Michael Colon, Bernd Finkbeiner, Mark Pichora, Henny B. Sipma, Tomas Uribe. An Update on STeP: Deductive-Algorithmic Verification of Reactive Systems. In Tool Support for System Specification, Development and Verification, Advances in Computing Science, pp 174-188, Springer Verlag, 1999.
Zohar Manna, Michael Colon, Bernd Finkbeiner, Henny Sipma, and Tomas Uribe. Abstraction and Modular Verification of Infinite-State Reactive Systems. Requirements Targeting Software and Systems Engineering (RTSE), LNCS 1526, Springer Verlag, pp 273-292, 1998.
Bernd Finkbeiner, Zohar Manna and Henny Sipma. Deductive Verification of Modular Systems. Compositionality: The Significant Difference, COMPOS'97, LNCS vol. 1536, pp 239-275, 1998.
Nikolaj Bjørner, Uri Lerner, and Zohar Manna. Deductive Verification of Parameterized Fault-Tolerant Systems: A Case Study. In Proc. of International Conference on Temporal Logic, Kluwer, July 1997.
Nikolaj Bjørner, Zohar Manna, Henny Sipma and Tomás Uribe. Deductive Verification of Real-time Systems using STeP, 4th International AMAST Workshop on Real-time Systems, LNCS vol 1231, Springer-Verlag, pp 22-43, 1997.
Nikolaj Bjorner, Anca Browne, Eddie Chang, Michael Colon, Arjun Kapur, Zohar Manna, Henny Sipma, Tomas Uribe, STeP: Deductive-Algorithmic Verification of Reactive and Real-time Systems, In 8th International Conference on Computer-Aided Verification, LNCS vol. 1102, pp. 415-418, Springer-Verlag, July 1996.
Nikolaj Bjorner, Anca Browne, Eddie Chang, Michael Colon, Arjun Kapur, Zohar Manna, Henny Sipma, Tomas Uribe, STeP: The Stanford Temporal Prover (Educational Release), User's Manual. Technical report STAN-CS-TR-95-1562, Computer Science Department, Stanford University, November 1995. Zohar Manna, Anuchit Anuchitanukul, Nikolaj Bjorner, Anca Browne, Edward Chang, Michael Colon, Luca de Alfaro, Harish Devarajan, Henny Sipma and Tomas Uribe, STeP: The Stanford Temporal Prover. Technical report STAN-CS-TR-94-1518, Computer Science Department, Stanford University, July 1994.
The STeP group. STeP: The Stanford Temporal Prover (2-page abstract). In TAPSOFT'95: Theory and Practice of Software Development, Lecture Notes in Computer Science 915, May 1995, pp. 793-794.

Miscellaneous

Henny Sipma. A Formal Model for Cross-Cutting Modular Transition Systems, Workshop on Foundations of Aspect-Oriented Languages (FOAL 2003), Boston, March 2003.
Alexandre M. Bayen, Pascal Grieder, Henny Sipma, George Meyer, and Claire J. Tomlin, Delay Predictive Models of the National Airspace System Using Hybrid Control Theory. In American Control Conference, WM pp 767-772, 2002.
Anuchit Anuchitanukul, Zohar Manna and Tomás E. Uribe. Differential BDDs. In J. van Leeuwen, ed, Computer Science Today , Lecture Notes in Computer Science, Vol. 1000, pp. 218-233, Springer-Verlag, Sep. 1995.

Last modified: Mon Feb 4 15:01:33 PST 2002