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.
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 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 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.
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.
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.
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. 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.
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.
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, 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.
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.
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.
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.
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.
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.
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.
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.
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.
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.