Selected Publications
(View by topic)
2007
- Ting Zhang, Henny B. Sipma, Zohar Manna, Verifying Balanced Trees.
To appear in LFCS.
- Cesar Sanchez, Henny B. Sipma, Zohar Manna, A Family of Distributed
Deadlock Avoidance Protocols and their Reachable State Spaces. To
appear in FASE.
- Cesar Sanchez, Henny B. Sipma, Zohar Manna, Generating Efficient
Distributed Deadlock Avoidance Controllers. To appear in WPDRTS.
2006
- Cesar Sanchez, Henny B. Sipma, Christopher G. Gill, Zohar Manna,
Distributed Priority Inheritance for Real-Time and Embedded
Systems. In 10th International Conference on Principles
of Distributed Systems (OPODIS), Lecture Notes in
Computer Science, Vol. 4305, Springer Verlag, pp 110-125, 2006.
- Matteo Slanina, Henny B. Sipma, and Zohar Manna,
Proving ATL* Properties of Infinite-State
Systems. In Theoretical Aspects of Computing (ICTAC),
Lecture Notes in Computer Science, Vol. 4281, Springer Verlag,
pp 242-256, 2006.
- 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. In Proceedings of
the 6th ACM & IEEE International conference on Embedded software
(EMSOFT), pp 252-261, 2006.
- Cesar Sanchez, Henny B. Sipma, Zohar Manna, Christopher D. Gill,
Efficient Distributed Deadlock Avoidance
with Liveness Guarantees. In Proceedings of
the 6th ACM & IEEE International conference on Embedded software
(EMSOFT), pp 12-20, 2006.
- 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.
- 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.
- 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.
- 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.
- 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.
2005
- 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.
- 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.
- 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.
- Ting Zhang, Henny B. Sipma, Zohar Manna,
The Decidability of the First-order Theory of Knuth-Bendix Order,
In Proc. of the 20th International Conference on
Automated Deduction (CADE'05), Tallinn, Estonia, July 2005,
Springer Verlag, LNCS 3632, pp 131-148.
- Aaron R. Bradley, Zohar Manna, Henny B. Sipma,
The Polyranking Principle,
In Proc. 32nd International Colloquium on Automata,
Languages and Programming, Lisboa, Portugal, July 2005,
Springer Verlag, LNCS 3580, pp 1349-1361.
- 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.
- 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.
- 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.
- Bernd Finkbeiner, Sriram Sankaranarayanan, and Henny B. Sipma,
Collecting statistics about runtime executions.
Formal Methods in System Design, Vol 27, No. 3, pp 253-274.
2004
- 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 .
- 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),
LNCS 3097, Springer Verlag, pp 152-167.
- Sriram Sankaranarayanan, Henny B. Sipma, Zohar Manna,
Constructing Invariants for Hybrid systems.
In Hybrid Systems: Computation and Control (HSCC 2004).
- Bernd Finkbeiner and Henny B. Sipma, Checking Finite Traces Using
Alternating Automata. In Formal Methods in System Design, vol 24,
pages 101-127.
- 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, 2004.
2003
- 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.
- 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
RT-DIA-80-2003, pages 83-98, Università di Roma Tre. Aracne Editrice, 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.
- Henny Sipma. A Formal Model for Cross-Cutting Modular Transition Systems,
Workshop on Foundations of Aspect-Oriented Languages (FOAL 2003), Boston,
March 2003.
2002
- Bernd Finkbeiner, Sriram Sankaranarayanan and Henny Sipma.
Collecting Statistics over Runtime Executions.
In RV'02.
- 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.
- 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.
2001
- Bernd Finkbeiner and Henny Sipma. Checking Finite Traces using Alternating Automata.
Workshop on Runtime Verification, CAV'01, 2001.
- 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.
- 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.
- 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.
2000
- 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.
- 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.
1999
- 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).
- 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.
- Henny Sipma.
Diagram-based verification of reactive,
real-time, and hybrid systems. PhD Thesis.
1998
- 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.
- 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.
- 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.
- 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.
- 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.
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.
- 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.
- 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.
1996
- 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.
- 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.
- 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.
1995
- 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 and Henny Sipma.
A Deductive Approach towards Controller Synthesis. In 1995 IEEE
International Symposium on Intelligent Control, Monterey, CA,
1995, pp. 35--41.
- 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).
-
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.
1994
-
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.
- 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.
Last modified: Mon Feb 4 15:01:33 PST 2002