Amir Pnueli
According to our database^{1}, Amir Pnueli
Awards
Turing Prize recipient
Turing Prize 1996, "For seminal work introducing temporal logic into computing science and for outstanding contributions to program and systems formal verificationverification.".
ACM Fellow
ACM Fellow 2007, "For contributions to program and system verification.".
Timeline
Legend:
Book In proceedings Article PhD thesis OtherLinks
Homepages:

at viaf.org

at isni.org

at id.loc.gov

at dnb.info

at dl.acm.org
On csauthors.net:
Bibliography
2012
Once and for all.
J. Comput. Syst. Sci., 2012
Synthesis of Reactive(1) designs.
J. Comput. Syst. Sci., 2012
Verification of multilinked heaps.
J. Comput. Syst. Sci., 2012
Low dimensional hybrid systems  decidable, undecidable, don't know.
Inf. Comput., 2012
Effective Synthesis of Asynchronous Systems from GR(1) Specifications.
Proceedings of the Verification, Model Checking, and Abstract Interpretation, 2012
2010
Revisiting Synthesis of GR(1) Specifications.
Proceedings of the Hardware and Software: Verification and Testing, 2010
Jtlv: A Framework for Developing Verification Algorithms.
Proceedings of the Computer Aided Verification, 22nd International Conference, 2010
Temporal Verification of Reactive Systems: Response.
Proceedings of the Time for Verification, 2010
Towards Component Based Design of Hybrid Systems: Safety and Stability.
Proceedings of the Time for Verification, 2010
Proving the Refuted: Symbolic Model Checkers as Proof Generators.
Proceedings of the Concurrency, 2010
2009
Synthesis of programs from temporal property specifications.
Proceedings of the 7th ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE 2009), 2009
Controller Synthesis from LSC Requirements.
Proceedings of the Fundamental Approaches to Software Engineering, 2009
2008
A Sound and Complete Deductive System for CTL* Verification.
Logic Journal of the IGPL, 2008
All You Need Is Compassion.
Proceedings of the Verification, 2008
On the Merits of Temporal Testers.
Proceedings of the 25 Years of Model Checking  History, Achievements, Perspectives, 2008
Program analysis for compiler validation.
Proceedings of the 8th ACM SIGPLANSIGSOFT Workshop on Program Analysis for Software Tools and Engineering, 2008
CoVaC: Compiler Validation by Program Analysis of the CrossProduct.
Proceedings of the FM 2008: Formal Methods, 2008
Discriminative Model Checking.
Proceedings of the Computer Aided Verification, 20th International Conference, 2008
Mechanical Verification of Transactional Memories with Nontransactional Memory Accesses.
Proceedings of the Computer Aided Verification, 20th International Conference, 2008
Checking Temporal Properties of Discrete, Timed and Continuous Behaviors.
Proceedings of the Pillars of Computer Science, 2008
Using Abstraction to Verify Arbitrary Temporal Properties.
Proceedings of the 15th AsiaPacific Software Engineering Conference (APSEC 2008), 2008
2007
Modular Ranking Abstraction.
Int. J. Found. Comput. Sci., 2007
Specify, Compile, Run: Hardware from PSL.
Electr. Notes Theor. Comput. Sci., 2007
Shape Analysis of SingleParent Heaps.
Proceedings of the Verification, 2007
"Don't Care" Modeling: A Logical Framework for Developing Predictive System Models.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2007
Synthesizing reactive systems from LSC requirements using the playengine.
Proceedings of the Companion to the 22nd Annual ACM SIGPLAN Conference on ObjectOriented Programming, 2007
Verifying Correctness of Transactional Memories.
Proceedings of the Formal Methods in ComputerAided Design, 7th International Conference, 2007
Interactive presentation: Automatic hardware synthesis from specifications: a case study.
Proceedings of the 2007 Design, Automation and Test in Europe Conference and Exposition, 2007
On Synthesizing Controllers from BoundedResponse Properties.
Proceedings of the Computer Aided Verification, 19th International Conference, 2007
2006
Liveness with invisible ranking.
STTT, 2006
Model Checking with Strong Fairness.
Formal Methods in System Design, 2006
Monitoring Interfaces for Faults.
Electr. Notes Theor. Comput. Sci., 2006
Reduced Functional Consistency of Uninterpreted Functions.
Electr. Notes Theor. Comput. Sci., 2006
Synthesis of Reactive(1) Designs.
Proceedings of the Verification, 2006
Ranking Abstraction of Recursive Programs.
Proceedings of the Verification, 2006
Faster Solutions of Rabin and Streett Games.
Proceedings of the 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 2006
Invisible Safety of Distributed Protocols.
Proceedings of the Automata, Languages and Programming, 33rd International Colloquium, 2006
Liveness by Invisible Invariants.
Proceedings of the Formal Techniques for Networked and Distributed Systems, 2006
From MITL to Timed Automata.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2006
PSL Model Checking and RunTime Verification Via Testers.
Proceedings of the FM 2006: Formal Methods, 2006
2005
A compositional approach to CTL* verification.
Theor. Comput. Sci., 2005
A discretetime UML semantics for concurrency and communication in safetycritical applications.
Sci. Comput. Program., 2005
Bridging the gap between fair simulation and trace inclusion.
Inf. Comput., 2005
Translation and RunTime Validation of Loop Transformations.
Formal Methods in System Design, 2005
Validating More Loop Optimizations.
Electr. Notes Theor. Comput. Sci., 2005
Abstraction for Liveness.
Proceedings of the Verification, 2005
Shape Analysis by Predicate Abstraction.
Proceedings of the Verification, 2005
Separating Fairness and WellFoundedness for the Analysis of Fair Discrete Systems.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005
Temporal Logic for ScenarioBased Specifications.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2005
Refining the Undecidability Frontier of Hybrid Automata.
Proceedings of the FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, 2005
Ranking Abstraction as Companion to Predicate Abstraction.
Proceedings of the Formal Techniques for Networked and Distributed Systems, 2005
Real Time Temporal Logic: Past, Present, Future.
Proceedings of the Formal Modeling and Analysis of Timed Systems, 2005
TVOC: A Translation Validator for Optimizing Compilers.
Proceedings of the Computer Aided Verification, 17th International Conference, 2005
IIV: An Invisible Invariant Verifier.
Proceedings of the Computer Aided Verification, 17th International Conference, 2005
Verification of Procedural Programs.
Proceedings of the We Will Show Them! Essays in Honour of Dov Gabbay, Volume Two, 2005
Synthesis Revisited: Generating Statechart Models from ScenarioBased Requirements.
Proceedings of the Formal Methods in Software and Systems Modeling, 2005
Ranking Abstraction as a Companion to Predicate Abstraction, .
Proceedings of the Automated Technology for Verification and Analysis, 2005
2004
Model checking and abstraction to the aid of parameterized systems (a survey).
Computer Languages, Systems & Structures, 2004
Liveness with Invisible Ranking.
Proceedings of the Verification, 2004
Deductive Verification of UML Models in TLPVS.
Proceedings of the «UML» 2004, 2004
Liveness with Incomprehensible Ranking.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2004
Smart PlayOut Extended: Time and Forbidden Elements.
Proceedings of the 4th International Conference on Quality Software (QSIC 2004), 2004
On Recognizable Timed Languages.
Proceedings of the Foundations of Software Science and Computation Structures, 2004
Range Allocation for Separation Logic.
Proceedings of the Computer Aided Verification, 16th International Conference, 2004
Validating the Translation of an Industrial Optimizing Compiler.
Proceedings of the Automated Technology for Verification and Analysis: Second International Conference, 2004
2003
VOC: A Methodology for the Translation Validation of OptimizingCompilers.
J. UCS, 2003
Erratum ("The small model property: how small can it be?" Volume 178, Number 1 [2002], pages 279293).
Inf. Comput., 2003
ModelChecking and Abstraction to the Aid of Parameterized Systems.
Proceedings of the Verification, 2003
Smart playout.
Proceedings of the Companion of the 18th Annual ACM SIGPLAN Conference on ObjectOriented Programming, 2003
Parameterized Verification by Probabilistic Abstraction.
Proceedings of the Foundations of Software Science and Computational Structures, 2003
Formal Modeling of C. elegans Development: A ScenarioBased Approach.
Proceedings of the Computational Methods in Systems Biology, First International Workshop, 2003
The ROBDD Size of Simple CNF Formulas.
Proceedings of the Correct Hardware Design and Verification Methods, 2003
Bridging the Gap between Fair Simulation and Trace Inclusion.
Proceedings of the Computer Aided Verification, 15th International Conference, 2003
TLPVS: A PVSBased LTL Verification System.
Proceedings of the Verification: Theory and Practice, 2003
2002
Complete Proof System for QPTL.
J. Log. Comput., 2002
The Small Model Property: How Small Can It Be?
Inf. Comput., 2002
Translation and RunTime Validation of Optimized Code.
Electr. Notes Theor. Comput. Sci., 2002
VOC: A Translation Validator for Optimizing Compilers.
Electr. Notes Theor. Comput. Sci., 2002
TimeC: A Time Constraint Language for ILP Processor Compilation.
Constraints, 2002
Automatic Verification of Probabilistic Free Choice.
Proceedings of the Verification, 2002
Applications of Formal Methods in Biology.
Proceedings of the Formal Techniques in RealTime and FaultTolerant Systems, 2002
Understanding UML: A Formal Semantics of Concurrency and Communication in RealTime UML.
Proceedings of the Formal Methods for Components and Objects, 2002
Smart Playout of Behavioral Requirements.
Proceedings of the Formal Methods in ComputerAided Design, 4th International Conference, 2002
Embedded Systems: Challenges in Specification and Verification.
Proceedings of the Embedded Software, Second International Conference, 2002
A Deductive Proof System for CTL.
Proceedings of the CONCUR 2002, 2002
Network Invariants in Action.
Proceedings of the CONCUR 2002, 2002
Liveness with (0, 1, infty)Counter Abstraction.
Proceedings of the Computer Aided Verification, 14th International Conference, 2002
Validating software pipelining optimizations.
Proceedings of the International Conference on Compilers, 2002
2001
Scheduling timeconstrained instructions on pipelined processors.
ACM Trans. Program. Lang. Syst., 2001
Symbolic model checking with rich assertional languages.
Theor. Comput. Sci., 2001
Verification by Augmented Abstraction: The AutomataTheoretic View.
J. Comput. Syst. Sci., 2001
Automatic Deductive Verification with Invisible Invariants.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2001
Sticks and stones: a coding scheme for parameterized verification.
Proceedings of the Twentieth Annual ACM Symposium on Principles of Distributed Computing, 2001
Range Allocation for Equivalence Logic.
Proceedings of the FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science, 2001
From Falsification to Verification.
Proceedings of the FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science, 2001
Beyond Regular Model Checking.
Proceedings of the FST TCS 2001: Foundations of Software Technology and Theoretical Computer Science, 2001
Parameterized Verification with Automatically Computed Inductive Assertions.
Proceedings of the Computer Aided Verification, 13th International Conference, 2001
2000
Control and Data Abstraction: The Cornerstones of Practical Formal Verification.
STTT, 2000
Propositional Temporal Logics: Decidability and Completeness.
Logic Journal of the IGPL, 2000
Verification by Augmented Finitary Abstraction.
Inf. Comput., 2000
Verification of Clocked and Hybrid Systems.
Acta Inf., 2000
A Comparison of Two Verification Methods for Speculative Instruction Execution.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 2000
Formal Verification of the RicartAgrawala Algorithm.
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 2000
Liveness and Acceleration in Parameterized Verification.
Proceedings of the Computer Aided Verification, 12th International Conference, 2000
Keynote Address: Abstraction, Composition, Symmetry, and a Little Deduction: The Remedies to State Explosion.
Proceedings of the Computer Aided Verification, 12th International Conference, 2000
Rigorous development of embedded systems.
Proceedings of the 2000 International Conference on Compilers, 2000
1999
Decidable Integration Graphs.
Inf. Comput., 1999
Proving Refinement Using Transduction.
Distributed Computing, 1999
Verifying Tomasulo's Algoithm by Refinement.
Proceedings of the 12th International Conference on VLSI Design (VLSI Design 1999), 1999
A Framework for Scheduler Synthesis.
Proceedings of the 20th IEEE RealTime Systems Symposium, 1999
Orthogonal Polyhedra: Representation and Computation.
Proceedings of the Hybrid Systems: Computation and Control, Second International Workshop, 1999
A Perfect Verification: Combining Model Checking with Deductive Analysis to Verify RealLife Software.
Proceedings of the FM'99  Formal Methods, 1999
Verifying Liveness by Augmented Abstraction.
Proceedings of the Computer Science Logic, 13th International Workshop, 1999
Deciding Equality Formulas by Small Domains Instantiations.
Proceedings of the Computer Aided Verification, 11th International Conference, 1999
Translation Validation: From SIGNAL to C.
Proceedings of the Correct System Design, 1999
1998
The Code Validation Tool CVT: Automatic Verification of a Compilation Process.
STTT, 1998
Translation Validation.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1998
Modularization and Abstraction: The Keys to Practical Formal Verification.
Proceedings of the Mathematical Foundations of Computer Science 1998, 1998
Translation Validation for Synchronous Languages.
Proceedings of the Automata, Languages and Programming, 25th International Colloquium, 1998
Algorithmic Verification of Linear Temporal Logic Specifications.
Proceedings of the Automata, Languages and Programming, 25th International Colloquium, 1998
Fair Synchronous Transition Systems and Their Liveness Proofs.
Proceedings of the Formal Techniques in RealTime and FaultTolerant Systems, 1998
Verification of DataInsensitive CIrcuits: An InOrderRetirement Case Study.
Proceedings of the Formal Methods in ComputerAided Design, 1998
Translation Validation: From DC+ to C*.
Proceedings of the Applied Formal Methods, 1998
Herbrand Automata for Hardware Verification.
Proceedings of the CONCUR '98: Concurrency Theory, 1998
On Discretization of Delays in Timed Automata and Digital Circuits.
Proceedings of the CONCUR '98: Concurrency Theory, 1998
Deductive vs. ModelTheoretic Approaches to Formal Verification (Abstract of Invited Talk).
Proceedings of the Automated Deduction, 1998
A Fast Algorithm for Scheduling TimeConstrained Instructions on Processors with ILP.
Proceedings of the 1998 International Conference on Parallel Architectures and Compilation Techniques, 1998
1997
Verification Engineering: A Future Profession (A. M. Turing Award Lecture).
Proceedings of the Sixteenth Annual ACM Symposium on Principles of Distributed Computing, 1997
Verifying Liveness Properties of Reactive Systems (Tutorial Abstract).
Proceedings of the Hybrid and RealTime Systems, 1997
DataStructures for the Verification of Timed Automata.
Proceedings of the Hybrid and RealTime Systems, 1997
Two Decades of Temporal Logic: Achievements and Challenges (Abstract).
Proceedings of the 38th Annual Symposium on Foundations of Computer Science, 1997
A Compositional RealTime Semantics of STATEMATE Designs.
Proceedings of the Compositionality: The Significant Difference, International Symposium, 1997
Verifying outoforder executions.
Proceedings of the Advances in Hardware Design and Verification, 1997
Symbolic Model Checking with Rich ssertional Languages.
Proceedings of the Computer Aided Verification, 9th International Conference, 1997
Some Progress in the Symbolic Verification of Timed Automata.
Proceedings of the Computer Aided Verification, 9th International Conference, 1997
1996
Verification of Clocked and Hybrid Systems.
Proceedings of the Lectures on Embedded Systems, European Educational Forum, 1996
A Platform for Combining Deductive with Algorithmic Verification.
Proceedings of the Computer Aided Verification, 8th International Conference, 1996
Using Ghost Variables to Prove Refinement.
Proceedings of the Algebraic Methodology and Software Technology, 1996
1995
On the Learnability of Infinitary Regular Sets
Inf. Comput., May, 1995
Reachability Analysis of Dynamical Systems Having PiecewiseConstant Derivatives.
Theor. Comput. Sci., 1995
On the Synthesis of Discrete Controllers for Timed Systems (An Extended Abstract).
STACS, 1995
Once and For All
Proceedings of the Proceedings, 1995
A Complete Proof Systems for QPTL
Proceedings of the Proceedings, 1995
Verifying Clocked Transition Systems.
Proceedings of the Hybrid Systems III: Verification and Control, 1995
Timing analysis of asynchronous circuits using timed automata.
Proceedings of the Correct Hardware Design and Verification Methods, 1995
Temporal verification of reactive systems  safety.
Springer, ISBN: 9780387944593, 1995
1994
Temporal Proof Methodologies for Timed Transition Systems
Inf. Comput., August, 1994
Proving Partial Order Properties.
Theor. Comput. Sci., 1994
Temporal Verification Diagrams.
Proceedings of the Theoretical Aspects of Computer Software, 1994
Compositional Verification of RealTime Systems
Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS '94), 1994
Symbolic Controller Synthesis for Discrete and Timed Systems.
Proceedings of the Hybrid Systems II, 1994
Development of Hybrid Systems.
Proceedings of the Formal Techniques in RealTime and FaultTolerant Systems, Third International Symposium Organized Jointly with the Working Group Provably Correct Systems, 1994
Prooving Safety Properties of Hybrid Systems.
Proceedings of the Formal Techniques in RealTime and FaultTolerant Systems, Third International Symposium Organized Jointly with the Working Group Provably Correct Systems, 1994
1993
Probabilistic Verification
Inf. Comput., March, 1993
Models for Reactivity.
Acta Inf., 1993
Temporal Verification of Simulation and Refinement.
Proceedings of the A Decade of Concurrency, Reflections and Perspectives, 1993
In and Out of Temporal Logic
Proceedings of the Eighth Annual Symposium on Logic in Computer Science (LICS '93), 1993
Reachability Analysis of Planar Multilimear Systems.
Proceedings of the Computer Aided Verification, 5th International Conference, 1993
A Decision Algorithm for Full Propositional Temporal Logic.
Proceedings of the Computer Aided Verification, 5th International Conference, 1993
1992
A Temporal Proof Methodology for Reactive Systems.
Proceedings of the Program Design Calculi, Proceedings of the NATO Advanced Study Institute on Program Design Calculi, Marktoberdorf, Germany, July 28, 1992
Time for Concurrency.
Proceedings of the Future Tendencies in Computer Science, 1992
What Good Are Digital Clocks?
Proceedings of the Automata, Languages and Programming, 19th International Colloquium, 1992
Characterization of Temporal Property Classes.
Proceedings of the Automata, Languages and Programming, 19th International Colloquium, 1992
Verifying Hybrid Systems.
Proceedings of the Hybrid Systems, 1992
Integration Graphs: A Class of Decidable Hybrid Systems.
Proceedings of the Hybrid Systems, 1992
Towards Refining Temporal Specifications into Hybrid Systems.
Proceedings of the Hybrid Systems, 1992
Timed and Hybrid Statecharts and Their Textual Representation.
Proceedings of the Formal Techniques in RealTime and FaultTolerant Systems, 1992
System Specification and Refinement in Temporal Logic.
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1992
How Vital is Liveness? Verifying Timing Properties of Reactive and Hybrid Systems (Extended Abstract).
Proceedings of the CONCUR '92, 1992
The temporal logic of reactive and concurrent systems  specification.
Springer, ISBN: 9783540976646, 1992
1991
Completing the Temporal Picture.
Theor. Comput. Sci., 1991
What is in a Step: On the Semantics of Statecharts.
Proceedings of the Theoretical Aspects of Computer Software, 1991
From Timed to Hybrid Systems.
Proceedings of the RealTime: Theory in Practice, 1991
Timed Transition Systems.
Proceedings of the RealTime: Theory in Practice, 1991
Communication with Directed Logic Variables.
Proceedings of the Conference Record of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, 1991
Temporal Proof Methodologies for Realtime Systems.
Proceedings of the Conference Record of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, 1991
On the Faithfulness of Formal Models.
Proceedings of the Mathematical Foundations of Computer Science 1991, 1991
Specifying and Proving Serializability in Temporal Logic
Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS '91), 1991
On the Learnability of Infinitary Regular Sets.
Proceedings of the Fourth Annual Workshop on Computational Learning Theory, 1991
1990
STATEMATE: A Working Environment for the Development of Complex Reactive Systems.
IEEE Trans. Software Eng., 1990
A Hierarchy of Temporal Properties.
Proceedings of the Ninth Annual ACM Symposium on Principles of Distributed Computing, 1990
Explicit Clock Temporal Logic
Proceedings of the Fifth Annual Symposium on Logic in Computer Science (LICS '90), 1990
A temporal proof methodology for reactive systems.
Proceedings of the Next Decade in Information Technology: Proceedings of the 5th Jerusalem Conference on Information Technology 1990, 1990
An interleaving model for realtime.
Proceedings of the Next Decade in Information Technology: Proceedings of the 5th Jerusalem Conference on Information Technology 1990, 1990
Proving Partial Order Liveness Properties.
Proceedings of the Automata, Languages and Programming, 17th International Colloquium, 1990
Distributed Reactive Systems Are Hard to Synthesize
Proceedings of the 31st Annual Symposium on Foundations of Computer Science, 1990
Tight Bounds on the Complexity of Cascaded Decomposition of Automata
Proceedings of the 31st Annual Symposium on Foundations of Computer Science, 1990
1989
On the Synthesis of a Reactive Module.
Proceedings of the Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, 1989
Specification and verification of VLSI systems.
Proceedings of the 1989 IEEE International Conference on ComputerAided Design, 1989
On the Synthesis of an Asynchronous Reactive Module.
Proceedings of the Automata, Languages and Programming, 16th International Colloquium, 1989
Completing the Temporal Picture.
Proceedings of the Automata, Languages and Programming, 16th International Colloquium, 1989
Learning omegaRegular Languages from Queries and CounterExamples (A Preliminary Report).
Proceedings of the Analogical and Inductive Inference, 1989
1988
The grammar of dimensions in machine drawings.
Computer Vision, Graphics, and Image Processing, 1988
The anchored version of the temporal framework.
Proceedings of the Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, School/Workshop, Noordwijkerhout, The Netherlands, May 30, 1988
STATEMATE; A Working Environment for the Development of Complex Reactive Systems.
Proceedings of the Proceedings, 1988
Applications of Temporal Logic to the Specification of Realtime Systems.
Proceedings of the Formal Techniques in RealTime and FaultTolerant Systems, 1988
A Framework for the Synthesis of Reactive Modules.
Proceedings of the Concurrency 88: International Conference on Concurrency, 1988
1987
Very High Level Concurrent Programming.
IEEE Trans. Software Eng., 1987
Specification and Verification of Concurrent Programs by forallAutomata.
Proceedings of the Temporal Logic in Specification, 1987
Specification and Implementation of Concurrently Accessed Data Structures: An Abstract Data Type Approach.
Proceedings of the STACS 87, 1987
Specification and Verification of Concurrent Programs By ForallAutomata.
Proceedings of the Conference Record of the Fourteenth Annual ACM Symposium on Principles of Programming Languages, 1987
A Hierarchy of Temporal Properties (Abstract).
Proceedings of the Sixth Annual ACM Symposium on Principles of Distributed Computing, 1987
On the Formal Semantics of Statecharts (Extended Abstract)
Proceedings of the Symposium on Logic in Computer Science (LICS '87), 1987
1986
Verification of Multiprocess Probabilistic Protocols.
Distributed Computing, 1986
A Really Abstract Concurrent Model and its Temporal Logic.
Proceedings of the Conference Record of the Thirteenth Annual ACM Symposium on Principles of Programming Languages, 1986
A Choppy Logic
Proceedings of the Symposium on Logic in Computer Science (LICS '86), 1986
Probabilistic Verification by Tableaux
Proceedings of the Symposium on Logic in Computer Science (LICS '86), 1986
Specification and Development of Reactive Systems (Invited Paper).
IFIP Congress, 1986
Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of Current Trends.
Proceedings of the Current Trends in Concurrency, Overviews and Tutorials, 1986
1985
Checking That Finite State Concurrent Programs Satisfy Their Linear Specification.
Proceedings of the Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, 1985
The Glory of the Past.
Proceedings of the Logics of Programs, 1985
Proving Termination of Prolog Programs.
Proceedings of the Logics of Programs, 1985
Linear and Branching Structures in the Semantics and Logics of Reactive Systems.
Proceedings of the Automata, 1985
1984
Automatic program generation in distributed cooperative computation.
IEEE Trans. Systems, Man, and Cybernetics, 1984
A LinearHistory Semantics for Languages for Distributed Programming.
Theor. Comput. Sci., 1984
Symmetric and Economical Solutions to the Mutual Exclusion Problem in a Distributed System.
Theor. Comput. Sci., 1984
Fair Termination RevisitedWith Delay.
Theor. Comput. Sci., 1984
Is the Interesting Part of Process Logic Uninteresting? A Translation from PL to PDL.
SIAM J. Comput., 1984
Verification of Probabilistic Programs.
SIAM J. Comput., 1984
Adequate Proof Principles for Invariance and Liveness Properties of Concurrent Programs.
Sci. Comput. Program., 1984
Now You May Compose Temporal Logic Specifications
Proceedings of the 16th Annual ACM Symposium on Theory of Computing, April 30, 1984
Temporal Verification of CarrierSense Local Area Network Protocols.
Proceedings of the Conference Record of the Eleventh Annual ACM Symposium on Principles of Programming Languages, 1984
Verification of Multiprocess Probabilistic Protocols.
Proceedings of the Third Annual ACM Symposium on Principles of Distributed Computing, 1984
A Hardware Implementation of the CSP Primitives and its Verification.
Proceedings of the Automata, 1984
On the scope of static checking in definitional languages.
Proceedings of the 1984 ACM Annual Conference on Computer Science: The fifth generation challenge, 1984
1983
Compilation of Nonprocedural Specifications into Computer Programs.
IEEE Trans. Software Eng., 1983
Termination of Probabilistic Concurrent Program.
ACM Trans. Program. Lang. Syst., 1983
Propositional Dynamic Logic of Nonregular Programs.
J. Comput. Syst. Sci., 1983
The Temporal Logic of Branching Time.
Acta Inf., 1983
On the Extremely Fair Treatment of Probabilistic Algorithms
Proceedings of the 15th Annual ACM Symposium on Theory of Computing, 1983
How to Cook a Temporal Proof System for Your Pet Language.
Proceedings of the Conference Record of the Tenth Annual ACM Symposium on Principles of Programming Languages, 1983
There Exit Decidable Context Free Propositional Dynamic Logics.
Proceedings of the Logics of Programs, 1983
Proving Precedence Properties: The Temporal Way.
Proceedings of the Automata, 1983
Symmetric and Economical Solutions to the Mutual Exclusion Problem in a Distributed System (Extended Abstract).
Proceedings of the Automata, 1983
Solutions to Problem No.2.
Proceedings of the Analysis of Concurrent Systems, 1983
1982
Deterministic Propositional Dynamic Logic: Finite Models, Complexity, and Completeness.
J. Comput. Syst. Sci., 1982
Is the Interesting Part of Process Logic Uninteresting  A Translation from PL to PDL.
Proceedings of the Conference Record of the Ninth Annual ACM Symposium on Principles of Programming Languages, 1982
Termination of Probabilistic Concurrent Programs.
Proceedings of the Conference Record of the Ninth Annual ACM Symposium on Principles of Programming Languages, 1982
1981
The Temporal Semantics of Concurrent Programs.
Theor. Comput. Sci., 1981
Automatic Programming of Finite State Linear Programs.
SIAM J. Comput., 1981
The Temporal Logic of Branching Time.
Proceedings of the Conference Record of the Eighth Annual ACM Symposium on Principles of Programming Languages, 1981
Verification of Concurrent Programs: Temporal Proof Principles.
Proceedings of the Logics of Programs, Workshop, Yorktown Heights, New York, May 1981, 1981
Further Results on Propositional Dynamic Logic of Nonregular Programs.
Proceedings of the Logics of Programs, Workshop, Yorktown Heights, New York, May 1981, 1981
Realizing an Equational Specification.
Proceedings of the Automata, 1981
Impartiality, Justice and Fairness: The Ethics of Concurrent Termination.
Proceedings of the Automata, 1981
Finite Models for Deterministic Propositional Dynamic Logic.
Proceedings of the Automata, 1981
Propositional Dynamic Logic of ContextFree Programs
Proceedings of the 22nd Annual Symposium on Foundations of Computer Science, 1981
1980
Synchronous Schemes and Their Decision Problems.
Proceedings of the Conference Record of the Seventh Annual ACM Symposium on Principles of Programming Languages, 1980
On the Temporal Basis of Fairness.
Proceedings of the Conference Record of the Seventh Annual ACM Symposium on Principles of Programming Languages, 1980
A Linear History Semantics for Distributed Languages (Extended Abstract)
Proceedings of the 21st Annual Symposium on Foundations of Computer Science, 1980
1979
Use of a Nonprocedural Specification Language and Associated Program Generator in Software Development.
ACM Trans. Program. Lang. Syst., 1979
The Temporal Semantics of Concurrent Programs.
Proceedings of the Semantics of Concurrent Computation, 1979
The Modal Logic of Programs.
Proceedings of the Automata, 1979
1978
A Proof Method for Cyclic Programs.
Acta Inf., 1978
1977
A Direct Algorithm for Checking Equivalence of LL(k) Grammars.
Theor. Comput. Sci., 1977
Backtracking in Recursive Computations.
Acta Inf., 1977
A Complete Axiomatic System for Proving Deductions about Recursive Programs
Proceedings of the 9th Annual ACM Symposium on Theory of Computing, 1977
Simple Programs and Their Decision Problems.
Proceedings of the Automata, 1977
The Temporal Logic of Programs
Proceedings of the 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October, 1977
1974
Axiomatic Approach to Total Correctness of Programs.
Acta Inf., 1974
1973
Decidable Properties of Monadic Functional Schemas.
J. ACM, 1973
1972
Permutation Graphs and Transitive Graphs.
J. ACM, 1972
1971
Marked Directed Graphs.
J. Comput. Syst. Sci., 1971
1970
Formalization of Properties of Functional Programs.
J. ACM, 1970
1969
Formalization of Properties of Recursively Defined Functions
Proceedings of the 1st Annual ACM Symposium on Theory of Computing, 1969