Selected publications of Henny Sipma

Selected Publications of Henny Sipma (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.
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, 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.
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, 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.

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, In Proc. of the 20th International Conference on Automated Deduction (CADE'05), Tallinn, Estonia, July 2005, Springer Verlag, LNCS 3632, pp 131-148.
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, 2004, pp 152-167.
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

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. Formal Methods in System Design, Vol 27, No. 3, pp 253-274, 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 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.
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.
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, 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, 2003, 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.
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.
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

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

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

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

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