| 2009 |
| 248 | EE | Hillel Kugler,
Cory Plock,
Amir Pnueli:
Controller Synthesis from LSC Requirements.
FASE 2009: 79-93 |
| 2008 |
| 247 | EE | Amir Pnueli,
Aleksandr Zaks:
On the Merits of Temporal Testers.
25 Years of Model Checking 2008: 172-195 |
| 246 | EE | Ariel Cohen,
Amir Pnueli,
Lenore D. Zuck:
Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses.
CAV 2008: 121-134 |
| 245 | EE | Peter Niebert,
Doron Peled,
Amir Pnueli:
Discriminative Model Checking.
CAV 2008: 504-516 |
| 244 | EE | Anna Zaks,
Amir Pnueli:
CoVaC: Compiler Validation by Program Analysis of the Cross-Product.
FM 2008: 35-51 |
| 243 | EE | Anna Zaks,
Amir Pnueli:
Program analysis for compiler validation.
PASTE 2008: 1-7 |
| 242 | EE | Oded Maler,
Dejan Nickovic,
Amir Pnueli:
Checking Temporal Properties of Discrete, Timed and Continuous Behaviors.
Pillars of Computer Science 2008: 475-505 |
| 241 | EE | Amir Pnueli,
Yaniv Sa'ar:
All You Need Is Compassion.
VMCAI 2008: 233-247 |
| 2007 |
| 240 | EE | Oded Maler,
Dejan Nickovic,
Amir Pnueli:
On Synthesizing Controllers from Bounded-Response Properties.
CAV 2007: 95-107 |
| 239 | EE | Roderick Bloem,
Stefan Galler,
Barbara Jobstmann,
Nir Piterman,
Amir Pnueli,
Martin Weiglhofer:
Interactive presentation: Automatic hardware synthesis from specifications: a case study.
DATE 2007: 1188-1193 |
| 238 | EE | Ariel Cohen,
John W. O'Leary,
Amir Pnueli,
Mark R. Tuttle,
Lenore D. Zuck:
Verifying Correctness of Transactional Memories.
FMCAD 2007: 37-44 |
| 237 | EE | Hillel Kugler,
Cory Plock,
Amir Pnueli:
Synthesizing reactive systems from LSC requirements using the play-engine.
OOPSLA Companion 2007: 801-802 |
| 236 | EE | Hillel Kugler,
Amir Pnueli,
Michael J. Stern,
E. Jane Albert Hubbard:
"Don't Care" Modeling: A Logical Framework for Developing Predictive System Models.
TACAS 2007: 343-357 |
| 235 | EE | Ittai Balaban,
Amir Pnueli,
Lenore D. Zuck:
Shape Analysis of Single-Parent Heaps.
VMCAI 2007: 91-105 |
| 234 | EE | Roderick Bloem,
Stefan Galler,
Barbara Jobstmann,
Nir Piterman,
Amir Pnueli,
Martin Weiglhofer:
Specify, Compile, Run: Hardware from PSL.
Electr. Notes Theor. Comput. Sci. 190(4): 3-16 (2007) |
| 233 | EE | Ittai Balaban,
Amir Pnueli,
Lenore D. Zuck:
Modular Ranking Abstraction.
Int. J. Found. Comput. Sci. 18(1): 5-44 (2007) |
| 2006 |
| 232 | EE | Amir Pnueli,
Aleksandr Zaks:
PSL Model Checking and Run-Time Verification Via Testers.
FM 2006: 573-586 |
| 231 | EE | Oded Maler,
Dejan Nickovic,
Amir Pnueli:
From MITL to Timed Automata.
FORMATS 2006: 274-289 |
| 230 | EE | Yi Fang,
Kenneth L. McMillan,
Amir Pnueli,
Lenore D. Zuck:
Liveness by Invisible Invariants.
FORTE 2006: 356-371 |
| 229 | EE | Ittai Balaban,
Amir Pnueli,
Lenore D. Zuck:
Invisible Safety of Distributed Protocols.
ICALP (2) 2006: 528-539 |
| 228 | EE | Nir Piterman,
Amir Pnueli:
Faster Solutions of Rabin and Streett Games.
LICS 2006: 275-284 |
| 227 | EE | Ittai Balaban,
Ariel Cohen,
Amir Pnueli:
Ranking Abstraction of Recursive Programs.
VMCAI 2006: 267-281 |
| 226 | EE | Nir Piterman,
Amir Pnueli,
Yaniv Sa'ar:
Synthesis of Reactive(1) Designs.
VMCAI 2006: 364-380 |
| 225 | EE | Amir Pnueli,
Ofer Strichman:
Reduced Functional Consistency of Uninterpreted Functions.
Electr. Notes Theor. Comput. Sci. 144(2): 53-65 (2006) |
| 224 | EE | Amir Pnueli,
Aleksandr Zaks,
Lenore D. Zuck:
Monitoring Interfaces for Faults.
Electr. Notes Theor. Comput. Sci. 144(4): 73-89 (2006) |
| 223 | EE | Yonit Kesten,
Amir Pnueli,
Li-on Raviv,
Elad Shahar:
Model Checking with Strong Fairness.
Formal Methods in System Design 28(1): 57-84 (2006) |
| 222 | EE | Yi Fang,
Nir Piterman,
Amir Pnueli,
Lenore D. Zuck:
Liveness with invisible ranking.
STTT 8(3): 261-279 (2006) |
| 2005 |
| 221 | EE | Amir Pnueli:
Ranking Abstraction as a Companion to Predicate Abstraction, .
ATVA 2005: 1 |
| 220 | EE | Clark W. Barrett,
Yi Fang,
Benjamin Goldberg,
Ying Hu,
Amir Pnueli,
Lenore D. Zuck:
TVOC: A Translation Validator for Optimizing Compilers.
CAV 2005: 291-295 |
| 219 | EE | Ittai Balaban,
Yi Fang,
Amir Pnueli,
Lenore D. Zuck:
IIV: An Invisible Invariant Verifier.
CAV 2005: 408-412 |
| 218 | EE | Oded Maler,
Dejan Nickovic,
Amir Pnueli:
Real Time Temporal Logic: Past, Present, Future.
FORMATS 2005: 2-16 |
| 217 | EE | Ittai Balaban,
Amir Pnueli,
Lenore D. Zuck:
Ranking Abstraction as Companion to Predicate Abstraction.
FORTE 2005: 1-12 |
| 216 | EE | Venkatesh Mysore,
Amir Pnueli:
Refining the Undecidability Frontier of Hybrid Automata.
FSTTCS 2005: 261-272 |
| 215 | EE | David Harel,
Hillel Kugler,
Amir Pnueli:
Synthesis Revisited: Generating Statechart Models from Scenario-Based Requirements.
Formal Methods in Software and Systems Modeling 2005: 309-324 |
| 214 | EE | Amir Pnueli,
Andreas Podelski,
Andrey Rybalchenko:
Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete Systems.
TACAS 2005: 124-139 |
| 213 | EE | Hillel Kugler,
David Harel,
Amir Pnueli,
Yuan Lu,
Yves Bontemps:
Temporal Logic for Scenario-Based Specifications.
TACAS 2005: 445-460 |
| 212 | EE | Amir Pnueli:
Abstraction for Liveness.
VMCAI 2005: 146-146 |
| 211 | EE | Ittai Balaban,
Amir Pnueli,
Lenore D. Zuck:
Shape Analysis by Predicate Abstraction.
VMCAI 2005: 164-180 |
| 210 | | Amir Pnueli:
Verification of Procedural Programs.
We Will Show Them! (2) 2005: 543-590 |
| 209 | EE | Ying Hu,
Clark W. Barrett,
Benjamin Goldberg,
Amir Pnueli:
Validating More Loop Optimizations.
Electr. Notes Theor. Comput. Sci. 141(2): 69-84 (2005) |
| 208 | EE | Lenore D. Zuck,
Amir Pnueli,
Benjamin Goldberg,
Clark W. Barrett,
Yi Fang,
Ying Hu:
Translation and Run-Time Validation of Loop Transformations.
Formal Methods in System Design 27(3): 335-360 (2005) |
| 207 | EE | Yonit Kesten,
Nir Piterman,
Amir Pnueli:
Bridging the gap between fair simulation and trace inclusion.
Inf. Comput. 200(1): 35-61 (2005) |
| 206 | EE | Werner Damm,
Bernhard Josko,
Amir Pnueli,
Angelika Votintseva:
A discrete-time UML semantics for concurrency and communication in safety-critical applications.
Sci. Comput. Program. 55(1-3): 81-115 (2005) |
| 205 | EE | Yonit Kesten,
Amir Pnueli:
A compositional approach to CTL* verification.
Theor. Comput. Sci. 331(2-3): 397-428 (2005) |
| 2004 |
| 204 | EE | I. Gordin,
Raya Leviathan,
Amir Pnueli:
Validating the Translation of an Industrial Optimizing Compiler.
ATVA 2004: 230-247 |
| 203 | EE | Muralidhar Talupur,
Nishant Sinha,
Ofer Strichman,
Amir Pnueli:
Range Allocation for Separation Logic.
CAV 2004: 148-161 |
| 202 | EE | Oded Maler,
Amir Pnueli:
On Recognizable Timed Languages.
FoSSaCS 2004: 348-362 |
| 201 | EE | David Harel,
Hillel Kugler,
Amir Pnueli:
Smart Play-Out Extended: Time and Forbidden Elements.
QSIC 2004: 2-10 |
| 200 | EE | Yi Fang,
Nir Piterman,
Amir Pnueli,
Lenore D. Zuck:
Liveness with Incomprehensible Ranking.
TACAS 2004: 482-496 |
| 199 | EE | Tamarah Arons,
Jozef Hooman,
Hillel Kugler,
Amir Pnueli,
Mark van der Zwaag:
Deductive Verification of UML Models in TLPVS.
UML 2004: 335-349 |
| 198 | EE | Yi Fang,
Nir Piterman,
Amir Pnueli,
Lenore D. Zuck:
Liveness with Invisible Ranking.
VMCAI 2004: 223-238 |
| 197 | EE | Lenore D. Zuck,
Amir Pnueli:
Model checking and abstraction to the aid of parameterized systems (a survey).
Computer Languages, Systems & Structures 30(3-4): 139-169 (2004) |
| 2003 |
| 196 | | Oded Maler,
Amir Pnueli:
Hybrid Systems: Computation and Control, 6th International Workshop, HSCC 2003 Prague, Czech Republic, April 3-5, 2003, Proceedings
Springer 2003 |
| 195 | EE | Yonit Kesten,
Nir Piterman,
Amir Pnueli:
Bridging the Gap between Fair Simulation and Trace Inclusion.
CAV 2003: 381-393 |
| 194 | EE | Michael Langberg,
Amir Pnueli,
Yoav Rodeh:
The ROBDD Size of Simple CNF Formulas.
CHARME 2003: 363-377 |
| 193 | EE | Na'aman Kam,
David Harel,
Hillel Kugler,
Rami Marelly,
Amir Pnueli,
E. Jane Albert Hubbard,
Michael J. Stern:
Formal Modeling of C. elegans Development: A Scenario-Based Approach.
CMSB 2003: 4-20 |
| 192 | EE | Tamarah Arons,
Amir Pnueli,
Lenore D. Zuck:
Parameterized Verification by Probabilistic Abstraction.
FoSSaCS 2003: 87-102 |
| 191 | EE | David Harel,
Hillel Kugler,
Rami Marelly,
Amir Pnueli:
Smart play-out.
OOPSLA Companion 2003: 68-69 |
| 190 | EE | Amir Pnueli,
Lenore D. Zuck:
Model-Checking and Abstraction to the Aid of Parameterized Systems.
VMCAI 2003: 4 |
| 189 | EE | Amir Pnueli,
Tamarah Arons:
TLPVS: A PVS-Based LTL Verification System.
Verification: Theory and Practice 2003: 598-625 |
| 188 | EE | Amir Pnueli,
Yoav Rodeh,
Ofer Strichman,
Michael Siegel:
Erratum ("The small model property: how small can it be?" Volume 178, Number 1 [2002], pages 279-293).
Inf. Comput. 184(1): 227 (2003) |
| 187 | EE | Lenore D. Zuck,
Amir Pnueli,
Benjamin Goldberg:
VOC: A Methodology for the Translation Validation of OptimizingCompilers.
J. UCS 9(3): 223-247 (2003) |
| 2002 |
| 186 | EE | Raya Leviathan,
Amir Pnueli:
Validating software pipelining optimizations.
CASES 2002: 280-287 |
| 185 | EE | Amir Pnueli,
Jessie Xu,
Lenore D. Zuck:
Liveness with (0, 1, infty)-Counter Abstraction.
CAV 2002: 107-122 |
| 184 | EE | Yonit Kesten,
Amir Pnueli,
Elad Shahar,
Lenore D. Zuck:
Network Invariants in Action.
CONCUR 2002: 101-115 |
| 183 | EE | Amir Pnueli,
Yonit Kesten:
A Deductive Proof System for CTL.
CONCUR 2002: 24-40 |
| 182 | EE | Amir Pnueli:
Embedded Systems: Challenges in Specification and Verification.
EMSOFT 2002: 1-14 |
| 181 | EE | David Harel,
Hillel Kugler,
Rami Marelly,
Amir Pnueli:
Smart Play-out of Behavioral Requirements.
FMCAD 2002: 378-398 |
| 180 | EE | Werner Damm,
Bernhard Josko,
Amir Pnueli,
Angelika Votintseva:
Understanding UML: A Formal Semantics of Concurrency and Communication in Real-Time UML.
FMCO 2002: 71-98 |
| 179 | EE | Amir Pnueli:
Applications of Formal Methods in Biology.
FTRTFT 2002: 81-82 |
| 178 | EE | Lenore D. Zuck,
Amir Pnueli,
Yonit Kesten:
Automatic Verification of Probabilistic Free Choice.
VMCAI 2002: 208-224 |
| 177 | | Allen Leung,
Krishna V. Palem,
Amir Pnueli:
TimeC: A Time Constraint Language for ILP Processor Compilation.
Constraints 7(2): 75-115 (2002) |
| 176 | EE | Lenore D. Zuck,
Amir Pnueli,
Yi Fang,
Benjamin Goldberg:
VOC: A Translation Validator for Optimizing Compilers.
Electr. Notes Theor. Comput. Sci. 65(2): (2002) |
| 175 | EE | Lenore D. Zuck,
Amir Pnueli,
Yi Fang,
Benjamin Goldberg,
Ying Hu:
Translation and Run-Time Validation of Optimized Code.
Electr. Notes Theor. Comput. Sci. 70(4): (2002) |
| 174 | EE | Amir Pnueli,
Yoav Rodeh,
Ofer Strichman,
Michael Siegel:
The Small Model Property: How Small Can It Be?
Inf. Comput. 178(1): 279-293 (2002) |
| 173 | EE | Yonit Kesten,
Amir Pnueli:
Complete Proof System for QPTL.
J. Log. Comput. 12(5): 701-745 (2002) |
| 2001 |
| 172 | EE | Tamarah Arons,
Amir Pnueli,
Sitvanit Ruah,
Jiazhao Xu,
Lenore D. Zuck:
Parameterized Verification with Automatically Computed Inductive Assertions.
CAV 2001: 221-234 |
| 171 | EE | Dana Fisman,
Amir Pnueli:
Beyond Regular Model Checking.
FSTTCS 2001: 156-170 |
| 170 | EE | Doron Peled,
Amir Pnueli,
Lenore D. Zuck:
From Falsification to Verification.
FSTTCS 2001: 292-304 |
| 169 | EE | Amir Pnueli,
Yoav Rodeh,
Ofer Strichman:
Range Allocation for Equivalence Logic.
FSTTCS 2001: 317-333 |
| 168 | EE | Amir Pnueli:
Sticks and stones: a coding scheme for parameterized verification.
PODC 2001: 14 |
| 167 | EE | Amir Pnueli,
Sitvanit Ruah,
Lenore D. Zuck:
Automatic Deductive Verification with Invisible Invariants.
TACAS 2001: 82-97 |
| 166 | EE | Allen Leung,
Krishna V. Palem,
Amir Pnueli:
Scheduling time-constrained instructions on pipelined processors.
ACM Trans. Program. Lang. Syst. 23(1): 73-103 (2001) |
| 165 | | Yonit Kesten,
Amir Pnueli,
Moshe Y. Vardi:
Verification by Augmented Abstraction: The Automata-Theoretic View.
J. Comput. Syst. Sci. 62(4): 668-690 (2001) |
| 164 | EE | Yonit Kesten,
Oded Maler,
Monica Marcus,
Amir Pnueli,
Elad Shahar:
Symbolic model checking with rich assertional languages.
Theor. Comput. Sci. 256(1-2): 93-112 (2001) |
| 2000 |
| 163 | EE | Amir Pnueli:
Rigorous development of embedded systems.
CASES 2000: 1 |
| 162 | | Amir Pnueli:
Keynote Address: Abstraction, Composition, Symmetry, and a Little Deduction: The Remedies to State Explosion.
CAV 2000: 1 |
| 161 | | Amir Pnueli,
Elad Shahar:
Liveness and Acceleration in Parameterized Verification.
CAV 2000: 328-343 |
| 160 | EE | Ekaterina Sedletsky,
Amir Pnueli,
Mordechai Ben-Ari:
Formal Verification of the Ricart-Agrawala Algorithm.
FSTTCS 2000: 325-335 |
| 159 | EE | Tamarah Arons,
Amir Pnueli:
A Comparison of Two Verification Methods for Speculative Instruction Execution.
TACAS 2000: 487-502 |
| 158 | EE | Yonit Kesten,
Zohar Manna,
Amir Pnueli:
Verification of Clocked and Hybrid Systems.
Acta Inf. 36(11): 837-912 (2000) |
| 157 | | Yonit Kesten,
Amir Pnueli:
Verification by Augmented Finitary Abstraction.
Inf. Comput. 163(1): 203-243 (2000) |
| 156 | EE | Orna Lichtenstein,
Amir Pnueli:
Propositional Temporal Logics: Decidability and Completeness.
Logic Journal of the IGPL 8(1): (2000) |
| 155 | EE | Yonit Kesten,
Amir Pnueli:
Control and Data Abstraction: The Cornerstones of Practical Formal Verification.
STTT 2(4): 328-342 (2000) |
| 1999 |
| 154 | EE | Amir Pnueli,
Yoav Rodeh,
Ofer Strichman,
Michael Siegel:
Deciding Equality Formulas by Small Domains Instantiations.
CAV 1999: 455-469 |
| 153 | | Yonit Kesten,
Amir Pnueli:
Verifying Liveness by Augmented Abstraction.
CSL 1999: 141-156 |
| 152 | EE | Amir Pnueli,
Ofer Strichman,
Michael Siegel:
Translation Validation: From SIGNAL to C.
Correct System Design 1999: 231-255 |
| 151 | EE | Olivier Bournez,
Oded Maler,
Amir Pnueli:
Orthogonal Polyhedra: Representation and Computation.
HSCC 1999: 46-60 |
| 150 | EE | Karine Altisen,
Gregor Gößler,
Amir Pnueli,
Joseph Sifakis,
Stavros Tripakis,
Sergio Yovine:
A Framework for Scheduler Synthesis.
IEEE Real-Time Systems Symposium 1999: 154-163 |
| 149 | EE | Tamarah Arons,
Amir Pnueli:
Verifying Tomasulo's Algoithm by Refinement.
VLSI Design 1999: 306-309 |
| 148 | EE | Yonit Kesten,
Amit Klein,
Amir Pnueli,
Gil Raanan:
A Perfect Verification: Combining Model Checking with Deductive Analysis to Verify Real-Life Software.
World Congress on Formal Methods 1999: 173-194 |
| 147 | EE | Bengt Jonsson,
Amir Pnueli,
Camilla Rump:
Proving Refinement Using Transduction.
Distributed Computing 12(2-3): 129-149 (1999) |
| 146 | | Yonit Kesten,
Amir Pnueli,
Joseph Sifakis,
Sergio Yovine:
Decidable Integration Graphs.
Inf. Comput. 150(2): 209-243 (1999) |
| 1998 |
| 145 | | Willem P. de Roever,
Hans Langmaack,
Amir Pnueli:
Compositionality: The Significant Difference, International Symposium, COMPOS'97, Bad Malente, Germany, September 8-12, 1997. Revised Lectures
Springer 1998 |
| 144 | EE | Amir Pnueli:
Deductive vs. Model-Theoretic Approaches to Formal Verification (Abstract of Invited Talk).
CADE 1998: 301 |
| 143 | EE | Eugene Asarin,
Oded Maler,
Amir Pnueli:
On Discretization of Delays in Timed Automata and Digital Circuits.
CONCUR 1998: 470-484 |
| 142 | EE | Werner Damm,
Amir Pnueli,
Sitvanit Ruah:
Herbrand Automata for Hardware Verification.
CONCUR 1998: 67-83 |
| 141 | | Amir Pnueli,
Ofer Strichman,
Michael Siegel:
Translation Validation: From DC+ to C*.
FM-Trends 1998: 137-150 |
| 140 | EE | Amir Pnueli,
Tamarah Arons:
Verification of Data-Insensitive CIrcuits: An In-Order-Retirement Case Study.
FMCAD 1998: 351-368 |
| 139 | EE | Amir Pnueli,
Natarajan Shankar,
Eli Singerman:
Fair Synchronous Transition Systems and Their Liveness Proofs.
FTRTFT 1998: 198-209 |
| 138 | EE | Yonit Kesten,
Amir Pnueli,
Li-on Raviv:
Algorithmic Verification of Linear Temporal Logic Specifications.
ICALP 1998: 1-16 |
| 137 | EE | Amir Pnueli,
Ofer Strichman,
Michael Siegel:
Translation Validation for Synchronous Languages.
ICALP 1998: 235-246 |
| 136 | EE | Allen Leung,
Krishna V. Palem,
Amir Pnueli:
A Fast Algorithm for Scheduling Time-Constrained Instructions on Processors with ILP.
IEEE PACT 1998: 158- |
| 135 | EE | Yonit Kesten,
Amir Pnueli:
Modularization and Abstraction: The Keys to Practical Formal Verification.
MFCS 1998: 54-71 |
| 134 | EE | Amir Pnueli,
Michael Siegel,
Eli Singerman:
Translation Validation.
TACAS 1998: 151-166 |
| 133 | EE | Amir Pnueli,
Ofer Strichman,
Michael Siegel:
The Code Validation Tool CVT: Automatic Verification of a Compilation Process.
STTT 2(2): 192-201 (1998) |
| 1997 |
| 132 | | Marius Bozga,
Oded Maler,
Amir Pnueli,
Sergio Yovine:
Some Progress in the Symbolic Verification of Timed Automata.
CAV 1997: 179-190 |
| 131 | | Yonit Kesten,
Oded Maler,
Monica Marcus,
Amir Pnueli,
Elad Shahar:
Symbolic Model Checking with Rich ssertional Languages.
CAV 1997: 424-435 |
| 130 | | Werner Damm,
Amir Pnueli:
Verifying out-of-order executions.
CHARME 1997: 23-47 |
| 129 | EE | Werner Damm,
Bernhard Josko,
Hardi Hungar,
Amir Pnueli:
A Compositional Real-Time Semantics of STATEMATE Designs.
COMPOS 1997: 186-238 |
| 128 | EE | Amir Pnueli:
Two Decades of Temporal Logic: Achievements and Challenges (Abstract).
FOCS 1997: 78 |
| 127 | | Amir Pnueli:
Verifying Liveness Properties of Reactive Systems (Tutorial Abstract).
HART 1997: 1 |
| 126 | | Eugene Asarin,
Marius Bozga,
Alain Kerbrat,
Oded Maler,
Amir Pnueli,
Anne Rasse:
Data-Structures for the Verification of Timed Automata.
HART 1997: 346-360 |
| 125 | | Amir Pnueli:
Verification Engineering: A Future Profession (A. M. Turing Award Lecture).
PODC 1997: 7 |
| 1996 |
| 124 | | Monica Marcus,
Amir Pnueli:
Using Ghost Variables to Prove Refinement.
AMAST 1996: 226-240 |
| 123 | | Amir Pnueli,
Elad Shahar:
A Platform for Combining Deductive with Algorithmic Verification.
CAV 1996: 184-195 |
| 122 | | Yonit Kesten,
Zohar Manna,
Amir Pnueli:
Verification of Clocked and Hybrid Systems.
European Educational Forum: School on Embedded Systems 1996: 4-73 |
| 1995 |
| 121 | | Oded Maler,
Amir Pnueli:
Timing analysis of asynchronous circuits using timed automata.
CHARME 1995: 189-205 |
| 120 | | Yonit Kesten,
Zohar Manna,
Amir Pnueli:
Verifying Clocked Transition Systems.
Hybrid Systems 1995: 13-40 |
| 119 | | Yonit Kesten,
Amir Pnueli:
A Complete Proof Systems for QPTL
LICS 1995: 2-12 |
| 118 | | Orna Kupferman,
Amir Pnueli:
Once and For All
LICS 1995: 25-35 |
| 117 | | Oded Maler,
Amir Pnueli,
Joseph Sifakis:
On the Synthesis of Discrete Controllers for Timed Systems (An Extended Abstract).
STACS 1995: 229-242 |
| 116 | | Oded Maler,
Amir Pnueli:
On the Learnability of Infinitary Regular Sets
Inf. Comput. 118(2): 316-326 (1995) |
| 115 | EE | Eugene Asarin,
Oded Maler,
Amir Pnueli:
Reachability Analysis of Dynamical Systems Having Piecewise-Constant Derivatives.
Theor. Comput. Sci. 138(1): 35-65 (1995) |
| 1994 |
| 114 | | Arjun Kapur,
Thomas A. Henzinger,
Zohar Manna,
Amir Pnueli:
Prooving Safety Properties of Hybrid Systems.
FTRTFT 1994: 431-454 |
| 113 | | Amir Pnueli:
Development of Hybrid Systems.
FTRTFT 1994: 77-85 |
| 112 | | Eugene Asarin,
Oded Maler,
Amir Pnueli:
Symbolic Controller Synthesis for Discrete and Timed Systems.
Hybrid Systems 1994: 1-20 |
| 111 | | Edward Y. Chang,
Zohar Manna,
Amir Pnueli:
Compositional Verification of Real-Time Systems
LICS 1994: 458-465 |
| 110 | | Zohar Manna,
Amir Pnueli:
Temporal Verification Diagrams.
TACS 1994: 726-765 |
| 109 | | Thomas A. Henzinger,
Zohar Manna,
Amir Pnueli:
Temporal Proof Methodologies for Timed Transition Systems
Inf. Comput. 112(2): 273-337 (1994) |
| 108 | | Doron Peled,
Amir Pnueli:
Proving Partial Order Properties.
Theor. Comput. Sci. 126(2): 143-182 (1994) |
| 1993 |
| 107 | | Oded Maler,
Amir Pnueli:
Reachability Analysis of Planar Multi-limear Systems.
CAV 1993: 194-209 |
| 106 | | Yonit Kesten,
Zohar Manna,
Hugh McGuire,
Amir Pnueli:
A Decision Algorithm for Full Propositional Temporal Logic.
CAV 1993: 97-109 |
| 105 | | Amir Pnueli,
Lenore D. Zuck:
In and Out of Temporal Logic
LICS 1993: 124-135 |
| 104 | | Yonit Kesten,
Zohar Manna,
Amir Pnueli:
Temporal Verification of Simulation and Refinement.
REX School/Symposium 1993: 273-346 |
| 103 | | Zohar Manna,
Amir Pnueli:
Models for Reactivity.
Acta Inf. 30(7): 609-678 (1993) |
| 102 | | Amir Pnueli,
Lenore D. Zuck:
Probabilistic Verification
Inf. Comput. 103(1): 1-29 (1993) |
| 1992 |
| 101 | | Zohar Manna,
Amir Pnueli:
Time for Concurrency.
25th Anniversary of INRIA 1992: 129-153 |
| 100 | | Amir Pnueli:
How Vital is Liveness? Verifying Timing Properties of Reactive and Hybrid Systems (Extended Abstract).
CONCUR 1992: 162-175 |
| 99 | | Amir Pnueli:
System Specification and Refinement in Temporal Logic.
FSTTCS 1992: 1-38 |
| 98 | | Yonit Kesten,
Amir Pnueli:
Timed and Hybrid Statecharts and Their Textual Representation.
FTRTFT 1992: 591-620 |
| 97 | | Yonit Kesten,
Amir Pnueli,
Joseph Sifakis,
Sergio Yovine:
Integration Graphs: A Class of Decidable Hybrid Systems.
Hybrid Systems 1992: 179-208 |
| 96 | | Zohar Manna,
Amir Pnueli:
Verifying Hybrid Systems.
Hybrid Systems 1992: 4-35 |
| 95 | | Thomas A. Henzinger,
Zohar Manna,
Amir Pnueli:
Towards Refining Temporal Specifications into Hybrid Systems.
Hybrid Systems 1992: 60-76 |
| 94 | | Edward Y. Chang,
Zohar Manna,
Amir Pnueli:
Characterization of Temporal Property Classes.
ICALP 1992: 474-486 |
| 93 | | Thomas A. Henzinger,
Zohar Manna,
Amir Pnueli:
What Good Are Digital Clocks?
ICALP 1992: 545-558 |
| 1991 |
| 92 | EE | Oded Maler,
Amir Pnueli:
On the Learnability of Infinitary Regular Sets.
COLT 1991: 128-136 |
| 91 | | Doron Peled,
Shmuel Katz,
Amir Pnueli:
Specifying and Proving Serializability in Temporal Logic
LICS 1991: 232-244 |
| 90 | | Zohar Manna,
Amir Pnueli:
On the Faithfulness of Formal Models.
MFCS 1991: 28-42 |
| 89 | | Alon Kleinman,
Yael Moscowitz,
Amir Pnueli,
Ehud Y. Shapiro:
Communication with Directed Logic Variables.
POPL 1991: 221-232 |
| 88 | | Thomas A. Henzinger,
Zohar Manna,
Amir Pnueli:
Temporal Proof Methodologies for Real-time Systems.
POPL 1991: 353-366 |
| 87 | | Thomas A. Henzinger,
Zohar Manna,
Amir Pnueli:
Timed Transition Systems.
REX Workshop 1991: 226-251 |
| 86 | | Oded Maler,
Zohar Manna,
Amir Pnueli:
From Timed to Hybrid Systems.
REX Workshop 1991: 447-484 |
| 85 | | Amir Pnueli,
M. Shalev:
What is in a Step: On the Semantics of Statecharts.
TACS 1991: 244-264 |
| 84 | | Zohar Manna,
Amir Pnueli:
Completing the Temporal Picture.
Theor. Comput. Sci. 83(1): 91-130 (1991) |
| 1990 |
| 83 | | Oded Maler,
Amir Pnueli:
Tight Bounds on the Complexity of Cascaded Decomposition of Automata
FOCS 1990: 672-682 |
| 82 | | Amir Pnueli,
Roni Rosner:
Distributed Reactive Systems Are Hard to Synthesize
FOCS 1990: 746-757 |
| 81 | | Doron Peled,
Amir Pnueli:
Proving Partial Order Liveness Properties.
ICALP 1990: 553-571 |
| 80 | | Eyal Harel,
Orna Lichtenstein,
Amir Pnueli:
Explicit Clock Temporal Logic
LICS 1990: 402-413 |
| 79 | EE | Zohar Manna,
Amir Pnueli:
A Hierarchy of Temporal Properties.
PODC 1990: 377-410 |
| 78 | EE | David Harel,
Hagi Lachover,
Amnon Naamad,
Amir Pnueli,
Michal Politi,
Rivi Sherman,
Aharon Shtull-Trauring,
Mark B. Trakhtenbrot:
STATEMATE: A Working Environment for the Development of Complex Reactive Systems.
IEEE Trans. Software Eng. 16(4): 403-414 (1990) |
| 1989 |
| 77 | | Behnam Banieqbal,
Howard Barringer,
Amir Pnueli:
Temporal Logic in Specification, Altrincham, UK, April 8-10, 1987, Proceedings
Springer 1989 |
| 76 | | Oded Maler,
Amir Pnueli:
Learning omega-Regular Languages from Queries and Counter-Examples (A Preliminary Report).
AII 1989: 161-170 |
| 75 | | Zohar Manna,
Amir Pnueli:
Completing the Temporal Picture.
ICALP 1989: 534-558 |
| 74 | | Amir Pnueli,
Roni Rosner:
On the Synthesis of an Asynchronous Reactive Module.
ICALP 1989: 652-671 |
| 73 | | Amir Pnueli,
Roni Rosner:
On the Synthesis of a Reactive Module.
POPL 1989: 179-190 |
| 1988 |
| 72 | | Amir Pnueli,
Roni Rosner:
A Framework for the Synthesis of Reactive Modules.
Concurrency 1988: 4-17 |
| 71 | | Amir Pnueli,
Eyal Harel:
Applications of Temporal Logic to the Specification of Real-time Systems.
FTRTFT 1988: 84-98 |
| 70 | | David Harel,
Hagi Lachover,
Amnon Naamad,
Amir Pnueli,
Michal Politi,
Rivi Sherman,
Aharon Shtull-Trauring:
STATEMATE; A Working Environment for the Development of Complex Reactive Systems.
ICSE 1988: 396-406 |
| 69 | | Zohar Manna,
Amir Pnueli:
The anchored version of the temporal framework.
REX Workshop 1988: 201-284 |
| 68 | EE | Dov Dori,
Amir Pnueli:
The grammar of dimensions in machine drawings.
Computer Vision, Graphics, and Image Processing 42(1): 1-18 (1988) |
| 1987 |
| 67 | | David Harel,
Amir Pnueli,
Jeanette P. Schmidt,
Rivi Sherman:
On the Formal Semantics of Statecharts (Extended Abstract)
LICS 1987: 54-64 |
| 66 | | Zohar Manna,
Amir Pnueli:
A Hierarchy of Temporal Properties (Abstract).
PODC 1987: 205 |
| 65 | | Zohar Manna,
Amir Pnueli:
Specification and Verification of Concurrent Programs By Forall-Automata.
POPL 1987: 1-12 |
| 64 | | S. Kaplan,
Amir Pnueli:
Specification and Implementation of Concurrently Accessed Data Structures: An Abstract Data Type Approach.
STACS 1987: 220-244 |
| 63 | | Zohar Manna,
Amir Pnueli:
Specification and Verification of Concurrent Programs by forall-Automata.
Temporal Logic in Specification 1987: 124-164 |
| 62 | | Yuan Shi,
Noah S. Prywes,
Boleslaw K. Szymanski,
Amir Pnueli:
Very High Level Concurrent Programming.
IEEE Trans. Software Eng. 13(9): 1038-1046 (1987) |
| 1986 |
| 61 | | Amir Pnueli:
Specification and Development of Reactive Systems (Invited Paper).
IFIP Congress 1986: 845-858 |
| 60 | | Roni Rosner,
Amir Pnueli:
A Choppy Logic
LICS 1986: 306-313 |
| 59 | | Amir Pnueli,
Lenore D. Zuck:
Probabilistic Verification by Tableaux
LICS 1986: 322-331 |
| 58 | | Howard Barringer,
Ruurd Kuiper,
Amir Pnueli:
A Really Abstract Concurrent Model and its Temporal Logic.
POPL 1986: 173-183 |
| 57 | | Amir Pnueli:
Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of Current Trends.
Current Trends in Concurrency 1986: 510-584 |
| 56 | | Amir Pnueli,
Lenore D. Zuck:
Verification of Multiprocess Probabilistic Protocols.
Distributed Computing 1(1): 53-72 (1986) |
| 1985 |
| 55 | | Amir Pnueli:
Linear and Branching Structures in the Semantics and Logics of Reactive Systems.
ICALP 1985: 15-32 |
| 54 | | Orna Lichtenstein,
Amir Pnueli,
Lenore D. Zuck:
The Glory of the Past.
Logic of Programs 1985: 196-218 |
| 53 | | Nissim Francez,
Orna Grumberg,
Shmuel Katz,
Amir Pnueli:
Proving Termination of Prolog Programs.
Logic of Programs 1985: 89-105 |
| 52 | | Orna Lichtenstein,
Amir Pnueli:
Checking That Finite State Concurrent Programs Satisfy Their Linear Specification.
POPL 1985: 97-107 |
| 1984 |
| 51 | EE | Boleslaw K. Szymanski,
Noah S. Prywes,
Evan D. Lock,
Amir Pnueli:
On the scope of static checking in definitional languages.
ACM Conference on Computer Science 1984: 197-207 |
| 50 | | Dorit Ron,
Flavia Rosemberg,
Amir Pnueli:
A Hardware Implementation of the CSP Primitives and its Verification.
ICALP 1984: 423-435 |
| 49 | | Amir Pnueli,
Lenore D. Zuck:
Verification of Multiprocess Probabilistic Protocols.
PODC 1984: 12-27 |
| 48 | | Dennis Shasha,
Amir Pnueli,
W. Ewald:
Temporal Verification of Carrier-Sense Local Area Network Protocols.
POPL 1984: 54-65 |
| 47 | | Howard Barringer,
Ruurd Kuiper,
Amir Pnueli:
Now You May Compose Temporal Logic Specifications
STOC 1984: 51-63 |
| 46 | | Micha Sharir,
Amir Pnueli,
Sergiu Hart:
Verification of Probabilistic Programs.
SIAM J. Comput. 13(2): 292-314 (1984) |
| 45 | | Rivi Sherman,
Amir Pnueli,
David Harel:
Is the Interesting Part of Process Logic Uninteresting? A Translation from PL to PDL.
SIAM J. Comput. 13(4): 825-839 (1984) |
| 44 | | Zohar Manna,
Amir Pnueli:
Adequate Proof Principles for Invariance and Liveness Properties of Concurrent Programs.
Sci. Comput. Program. 4(3): 257-289 (1984) |
| 43 | | Nissim Francez,
Daniel J. Lehmann,
Amir Pnueli:
A Linear-History Semantics for Languages for Distributed Programming.
Theor. Comput. Sci. 32: 25-46 (1984) |
| 42 | | Krzysztof R. Apt,
Amir Pnueli,
Jonathan Stavi:
Fair Termination Revisited-With Delay.
Theor. Comput. Sci. 33: 65-84 (1984) |
| 41 | | Shimon Cohen,
Daniel J. Lehmann,
Amir Pnueli:
Symmetric and Economical Solutions to the Mutual Exclusion Problem in a Distributed System.
Theor. Comput. Sci. 34: 215-225 (1984) |
| 1983 |
| 40 | | Shimon Cohen,
Daniel J. Lehmann,
Amir Pnueli:
Symmetric and Economical Solutions to the Mutual Exclusion Problem in a Distributed System (Extended Abstract).
ICALP 1983: 128-136 |
| 39 | | Zohar Manna,
Amir Pnueli:
Proving Precedence Properties: The Temporal Way.
ICALP 1983: 491-512 |
| 38 | | Tmima Koren,
Amir Pnueli:
There Exit Decidable Context Free Propositional Dynamic Logics.
Logic of Programs 1983: 290-312 |
| 37 | | Zohar Manna,
Amir Pnueli:
How to Cook a Temporal Proof System for Your Pet Language.
POPL 1983: 141-154 |
| 36 | | Amir Pnueli:
On the Extremely Fair Treatment of Probabilistic Algorithms
STOC 1983: 278-290 |
| 35 | | Amir Pnueli:
Solutions to Problem No.2.
The Analysis of Concurrent Systems 1983: 365-383 |
| 34 | EE | Sergiu Hart,
Micha Sharir,
Amir Pnueli:
Termination of Probabilistic Concurrent Program.
ACM Trans. Program. Lang. Syst. 5(3): 356-380 (1983) |
| 33 | | Mordechai Ben-Ari,
Amir Pnueli,
Zohar Manna:
The Temporal Logic of Branching Time.
Acta Inf. 20: 207-226 (1983) |
| 32 | | Noah S. Prywes,
Amir Pnueli:
Compilation of Nonprocedural Specifications into Computer Programs.
IEEE Trans. Software Eng. 9(3): 267-279 (1983) |
| 31 | | David Harel,
Amir Pnueli,
Jonathan Stavi:
Propositional Dynamic Logic of Nonregular Programs.
J. Comput. Syst. Sci. 26(2): 222-243 (1983) |
| 1982 |
| 30 | | Sergiu Hart,
Micha Sharir,
Amir Pnueli:
Termination of Probabilistic Concurrent Programs.
POPL 1982: 1-6 |
| 29 | | Rivi Sherman,
Amir Pnueli,
David Harel:
Is the Interesting Part of Process Logic Uninteresting - A Translation from PL to PDL.
POPL 1982: 347-360 |
| 28 | | Mordechai Ben-Ari,
Joseph Y. Halpern,
Amir Pnueli:
Deterministic Propositional Dynamic Logic: Finite Models, Complexity, and Completeness.
J. Comput. Syst. Sci. 25(3): 402-417 (1982) |
| 1981 |
| 27 | | David Harel,
Amir Pnueli,
Jonathan Stavi:
Propositional Dynamic Logic of Context-Free Programs
FOCS 1981: 310-321 |
| 26 | | Mordechai Ben-Ari,
Joseph Y. Halpern,
Amir Pnueli:
Finite Models for Deterministic Propositional Dynamic Logic.
ICALP 1981: 249-263 |
| 25 | | Daniel J. Lehmann,
Amir Pnueli,
Jonathan Stavi:
Impartiality, Justice and Fairness: The Ethics of Concurrent Termination.
ICALP 1981: 264-277 |
| 24 | | Amir Pnueli,
R. Zarhi:
Realizing an Equational Specification.
ICALP 1981: 459-478 |
| 23 | | David Harel,
Amir Pnueli,
Jonathan Stavi:
Further Results on Propositional Dynamic Logic of Nonregular Programs.
Logic of Programs 1981: 124-136 |
| 22 | | Zohar Manna,
Amir Pnueli:
Verification of Concurrent Programs: Temporal Proof Principles.
Logic of Programs 1981: 200-252 |
| 21 | | Mordechai Ben-Ari,
Zohar Manna,
Amir Pnueli:
The Temporal Logic of Branching Time.
POPL 1981: 164-176 |
| 20 | | Amir Pnueli,
Giora Slutzki:
Automatic Programming of Finite State Linear Programs.
SIAM J. Comput. 10(3): 519-535 (1981) |
| 19 | | Amir Pnueli:
The Temporal Semantics of Concurrent Programs.
Theor. Comput. Sci. 13: 45-60 (1981) |
| 1980 |
| 18 | | Nissim Francez,
Daniel J. Lehmann,
Amir Pnueli:
A Linear History Semantics for Distributed Languages (Extended Abstract)
FOCS 1980: 143-151 |
| 17 | | Dov M. Gabbay,
Amir Pnueli,
Saharon Shelah,
Jonathan Stavi:
On the Temporal Basis of Fairness.
POPL 1980: 163-173 |
| 16 | | Zohar Manna,
Amir Pnueli:
Synchronous Schemes and Their Decision Problems.
POPL 1980: 62-67 |
| 1979 |
| 15 | | Zohar Manna,
Amir Pnueli:
The Modal Logic of Programs.
ICALP 1979: 385-409 |
| 14 | | Amir Pnueli:
The Temporal Semantics of Concurrent Programs.
Semantics of Concurrent Computation 1979: 1-20 |
| 13 | EE | Noah S. Prywes,
Amir Pnueli,
S. Shastry:
Use of a Nonprocedural Specification Language and Associated Program Generator in Software Development.
ACM Trans. Program. Lang. Syst. 1(2): 196-217 (1979) |
| 1978 |
| 12 | | Nissim Francez,
Amir Pnueli:
A Proof Method for Cyclic Programs.
Acta Inf. 9: 133-157 (1978) |
| 1977 |
| 11 | | Amir Pnueli:
The Temporal Logic of Programs
FOCS 1977: 46-57 |
| 10 | | Amir Pnueli,
Giora Slutzki:
Simple Programs and Their Decision Problems.
ICALP 1977: 380-390 |
| 9 | | David Harel,
Amir Pnueli,
Jonathan Stavi:
A Complete Axiomatic System for Proving Deductions about Recursive Programs
STOC 1977: 249-260 |
| 8 | | Nissim Francez,
Boris Klebansky,
Amir Pnueli:
Backtracking in Recursive Computations
Acta Inf. 8: 125-144 (1977) |
| 7 | | Tmima Olshansky,
Amir Pnueli:
A Direct Algorithm for Checking Equivalence of LL(k) Grammars.
Theor. Comput. Sci. 4(3): 321-349 (1977) |
| 1974 |
| 6 | | Zohar Manna,
Amir Pnueli:
Axiomatic Approach to Total Correctness of Programs
Acta Inf. 3: 243-263 (1974) |
| 1973 |
| 5 | EE | Edward A. Ashcroft,
Zohar Manna,
Amir Pnueli:
Decidable Properties of Monadic Functional Schemas.
J. ACM 20(3): 489-499 (1973) |
| 1972 |
| 4 | EE | Shimon Even,
Amir Pnueli,
Abraham Lempel:
Permutation Graphs and Transitive Graphs.
J. ACM 19(3): 400-410 (1972) |
| 1971 |
| 3 | | F. Commoner,
Anatol W. Holt,
Shimon Even,
Amir Pnueli:
Marked Directed Graphs.
J. Comput. Syst. Sci. 5(5): 511-523 (1971) |
| 1970 |
| 2 | EE | Zohar Manna,
Amir Pnueli:
Formalization of Properties of Functional Programs.
J. ACM 17(3): 555-569 (1970) |
| 1969 |
| 1 | | Zohar Manna,
Amir Pnueli:
Formalization of Properties of Recursively Defined Functions
STOC 1969: 201-210 |