


default search action
Amir Pnueli
Person information
- award (1996): Turing Award
- award (2007): ACM Software System Award
Refine list

refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2010 – 2019
- 2019
- [j64]Thomas Ferrère, Oded Maler, Dejan Nickovic
, Amir Pnueli:
From Real-time Logic to Timed Automata. J. ACM 66(3): 19:1-19:31 (2019) - 2018
- [p3]Nir Piterman, Amir Pnueli:
Temporal Logic and Fair Discrete Systems. Handbook of Model Checking 2018: 27-73 - 2012
- [j63]Eugene Asarin
, Venkatesh Mysore, Amir Pnueli, Gerardo Schneider:
Low dimensional hybrid systems - decidable, undecidable, don't know. Inf. Comput. 211: 138-159 (2012) - [j62]Ittai Balaban, Amir Pnueli, Yaniv Sa'ar, Lenore D. Zuck:
Verification of multi-linked heaps. J. Comput. Syst. Sci. 78(3): 853-876 (2012) - [j61]Roderick Bloem
, Barbara Jobstmann, Nir Piterman
, Amir Pnueli, Yaniv Sa'ar:
Synthesis of Reactive(1) designs. J. Comput. Syst. Sci. 78(3): 911-938 (2012) - [j60]Orna Kupferman, Amir Pnueli, Moshe Y. Vardi:
Once and for all. J. Comput. Syst. Sci. 78(3): 981-996 (2012) - [c204]Uri Klein, Nir Piterman
, Amir Pnueli:
Effective Synthesis of Asynchronous Systems from GR(1) Specifications. VMCAI 2012: 283-298 - 2010
- [c203]Werner Damm, Henning Dierks, Jens Oehlerking, Amir Pnueli:
Towards Component Based Design of Hybrid Systems: Safety and Stability. Essays in Memory of Amir Pnueli 2010: 96-143 - [c202]Ittai Balaban, Amir Pnueli, Lenore D. Zuck:
Proving the Refuted: Symbolic Model Checkers as Proof Generators. Concurrency, Compositionality, and Correctness 2010: 221-236 - [c201]Zohar Manna, Amir Pnueli:
Temporal Verification of Reactive Systems: Response. Essays in Memory of Amir Pnueli 2010: 279-361 - [c200]Amir Pnueli, Yaniv Sa'ar, Lenore D. Zuck:
Jtlv: A Framework for Developing Verification Algorithms. CAV 2010: 171-174 - [c199]Uri Klein, Amir Pnueli:
Revisiting Synthesis of GR(1) Specifications. Haifa Verification Conference 2010: 161-181 - [e4]Amir Pnueli, Irina B. Virbitskaite, Andrei Voronkov:
Perspectives of Systems Informatics, 7th International Andrei Ershov Memorial Conference, PSI 2009, Novosibirsk, Russia, June 15-19, 2009. Revised Papers. Lecture Notes in Computer Science 5947, Springer 2010, ISBN 978-3-642-11485-4 [contents]
2000 – 2009
- 2009
- [c198]Hillel Kugler
, Cory Plock, Amir Pnueli:
Controller Synthesis from LSC Requirements. FASE 2009: 79-93 - [c197]Amir Pnueli, Uri Klein:
Synthesis of programs from temporal property specifications. MEMOCODE 2009: 1-7 - 2008
- [j59]Dov M. Gabbay, Amir Pnueli:
A Sound and Complete Deductive System for CTL* Verification. Log. J. IGPL 16(6): 499-536 (2008) - [c196]Amir Pnueli:
Using Abstraction to Verify Arbitrary Temporal Properties. APSEC 2008: 3 - [c195]Oded Maler, Dejan Nickovic, Amir Pnueli:
Checking Temporal Properties of Discrete, Timed and Continuous Behaviors. Pillars of Computer Science 2008: 475-505 - [c194]Ariel Cohen, Amir Pnueli, Lenore D. Zuck:
Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses. CAV 2008: 121-134 - [c193]Peter Niebert, Doron A. Peled, Amir Pnueli:
Discriminative Model Checking. CAV 2008: 504-516 - [c192]Anna Zaks, Amir Pnueli:
CoVaC: Compiler Validation by Program Analysis of the Cross-Product. FM 2008: 35-51 - [c191]Anna Zaks, Amir Pnueli:
Program analysis for compiler validation. PASTE 2008: 1-7 - [c190]Amir Pnueli, Aleksandr Zaks:
On the Merits of Temporal Testers. 25 Years of Model Checking 2008: 172-195 - [c189]Amir Pnueli, Yaniv Sa'ar:
All You Need Is Compassion. VMCAI 2008: 233-247 - 2007
- [j58]Ittai Balaban, Amir Pnueli, Lenore D. Zuck:
Modular Ranking Abstraction. Int. J. Found. Comput. Sci. 18(1): 5-44 (2007) - [c188]Oded Maler, Dejan Nickovic, Amir Pnueli:
On Synthesizing Controllers from Bounded-Response Properties. CAV 2007: 95-107 - [c187]Roderick Bloem
, Stefan J. Galler, Barbara Jobstmann, Nir Piterman, Amir Pnueli, Martin Weiglhofer:
Interactive presentation: Automatic hardware synthesis from specifications: a case study. DATE 2007: 1188-1193 - [c186]Ariel Cohen, John W. O'Leary, Amir Pnueli, Mark R. Tuttle, Lenore D. Zuck:
Verifying Correctness of Transactional Memories. FMCAD 2007: 37-44 - [c185]Hillel Kugler
, Cory Plock, Amir Pnueli:
Synthesizing reactive systems from LSC requirements using the play-engine. OOPSLA Companion 2007: 801-802 - [c184]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 - [c183]Ittai Balaban, Amir Pnueli, Lenore D. Zuck:
Shape Analysis of Single-Parent Heaps. VMCAI 2007: 91-105 - [c182]Roderick Bloem
, Stefan J. Galler, Barbara Jobstmann, Nir Piterman
, Amir Pnueli, Martin Weiglhofer:
Specify, Compile, Run: Hardware from PSL. COCV@ETAPS 2007: 3-16 - 2006
- [j57]Yonit Kesten, Amir Pnueli, Li-on Raviv, Elad Shahar:
Model Checking with Strong Fairness. Formal Methods Syst. Des. 28(1): 57-84 (2006) - [j56]Yi Fang, Nir Piterman
, Amir Pnueli, Lenore D. Zuck:
Liveness with invisible ranking. Int. J. Softw. Tools Technol. Transf. 8(3): 261-279 (2006) - [c181]Amir Pnueli, Aleksandr Zaks:
PSL Model Checking and Run-Time Verification Via Testers. FM 2006: 573-586 - [c180]Oded Maler, Dejan Nickovic, Amir Pnueli:
From MITL to Timed Automata. FORMATS 2006: 274-289 - [c179]Yi Fang, Kenneth L. McMillan, Amir Pnueli, Lenore D. Zuck:
Liveness by Invisible Invariants. FORTE 2006: 356-371 - [c178]Ittai Balaban, Amir Pnueli, Lenore D. Zuck:
Invisible Safety of Distributed Protocols. ICALP (2) 2006: 528-539 - [c177]Nir Piterman
, Amir Pnueli:
Faster Solutions of Rabin and Streett Games. LICS 2006: 275-284 - [c176]Ittai Balaban, Ariel Cohen, Amir Pnueli:
Ranking Abstraction of Recursive Programs. VMCAI 2006: 267-281 - [c175]Nir Piterman, Amir Pnueli, Yaniv Sa'ar:
Synthesis of Reactive(1) Designs. VMCAI 2006: 364-380 - 2005
- [j55]Lenore D. Zuck, Amir Pnueli, Benjamin Goldberg, Clark W. Barrett
, Yi Fang, Ying Hu:
Translation and Run-Time Validation of Loop Transformations. Formal Methods Syst. Des. 27(3): 335-360 (2005) - [j54]Yonit Kesten, Nir Piterman
, Amir Pnueli:
Bridging the gap between fair simulation and trace inclusion. Inf. Comput. 200(1): 35-61 (2005) - [j53]Werner Damm, Bernhard Josko, Amir Pnueli, Anjelika Votintseva:
A discrete-time UML semantics for concurrency and communication in safety-critical applications. Sci. Comput. Program. 55(1-3): 81-115 (2005) - [j52]Yonit Kesten, Amir Pnueli:
A compositional approach to CTL* verification. Theor. Comput. Sci. 331(2-3): 397-428 (2005) - [c174]Amir Pnueli:
Ranking Abstraction as a Companion to Predicate Abstraction, . ATVA 2005: 1 - [c173]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 - [c172]Amir Pnueli:
Verification of Procedural Programs. We Will Show Them! (2) 2005: 543-590 - [c171]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 - [c170]Ittai Balaban, Yi Fang, Amir Pnueli, Lenore D. Zuck:
IIV: An Invisible Invariant Verifier. CAV 2005: 408-412 - [c169]Oded Maler, Dejan Nickovic, Amir Pnueli:
Real Time Temporal Logic: Past, Present, Future. FORMATS 2005: 2-16 - [c168]Ittai Balaban, Amir Pnueli, Lenore D. Zuck:
Ranking Abstraction as Companion to Predicate Abstraction. FORTE 2005: 1-12 - [c167]Venkatesh Mysore, Amir Pnueli:
Refining the Undecidability Frontier of Hybrid Automata. FSTTCS 2005: 261-272 - [c166]Amir Pnueli, Andreas Podelski, Andrey Rybalchenko:
Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete Systems. TACAS 2005: 124-139 - [c165]Hillel Kugler, David Harel, Amir Pnueli, Yuan Lu, Yves Bontemps:
Temporal Logic for Scenario-Based Specifications. TACAS 2005: 445-460 - [c164]Amir Pnueli:
Abstraction for Liveness. VMCAI 2005: 146-146 - [c163]Ittai Balaban, Amir Pnueli, Lenore D. Zuck:
Shape Analysis by Predicate Abstraction. VMCAI 2005: 164-180 - [c162]Amir Pnueli, Ofer Strichman
:
Reduced Functional Consistency of Uninterpreted Functions. PDPAR@CAV 2005: 53-65 - [c161]Ying Hu, Clark W. Barrett
, Benjamin Goldberg, Amir Pnueli:
Validating More Loop Optimizations. COCV@ETAPS 2005: 69-84 - [c160]Amir Pnueli, Aleksandr Zaks, Lenore D. Zuck:
Monitoring Interfaces for Faults. RV@CAV 2005: 73-89 - 2004
- [j51]Lenore D. Zuck, Amir Pnueli:
Model checking and abstraction to the aid of parameterized systems (a survey). Comput. Lang. Syst. Struct. 30(3-4): 139-169 (2004) - [c159]I. Gordin, Raya Leviathan, Amir Pnueli:
Validating the Translation of an Industrial Optimizing Compiler. ATVA 2004: 230-247 - [c158]Muralidhar Talupur, Nishant Sinha, Ofer Strichman
, Amir Pnueli:
Range Allocation for Separation Logic. CAV 2004: 148-161 - [c157]Oded Maler, Amir Pnueli:
On Recognizable Timed Languages. FoSSaCS 2004: 348-362 - [c156]David Harel, Hillel Kugler
, Amir Pnueli:
Smart Play-Out Extended: Time and Forbidden Elements. QSIC 2004: 2-10 - [c155]Yi Fang, Nir Piterman, Amir Pnueli, Lenore D. Zuck:
Liveness with Incomprehensible Ranking. TACAS 2004: 482-496 - [c154]Tamarah Arons, Jozef Hooman, Hillel Kugler, Amir Pnueli, Mark van der Zwaag:
Deductive Verification of UML Models in TLPVS. UML 2004: 335-349 - [c153]Yi Fang, Nir Piterman, Amir Pnueli, Lenore D. Zuck:
Liveness with Invisible Ranking. VMCAI 2004: 223-238 - 2003
- [j50]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) - [j49]Lenore D. Zuck, Amir Pnueli, Benjamin Goldberg:
VOC: A Methodology for the Translation Validation of OptimizingCompilers. J. Univers. Comput. Sci. 9(3): 223-247 (2003) - [c152]Amir Pnueli, Tamarah Arons:
TLPVS: A PVS-Based LTL Verification System. Verification: Theory and Practice 2003: 598-625 - [c151]Yonit Kesten, Nir Piterman, Amir Pnueli:
Bridging the Gap between Fair Simulation and Trace Inclusion. CAV 2003: 381-393 - [c150]Michael Langberg, Amir Pnueli, Yoav Rodeh:
The ROBDD Size of Simple CNF Formulas. CHARME 2003: 363-377 - [c149]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 - [c148]Tamarah Arons, Amir Pnueli, Lenore D. Zuck:
Parameterized Verification by Probabilistic Abstraction. FoSSaCS 2003: 87-102 - [c147]David Harel, Hillel Kugler
, Rami Marelly, Amir Pnueli:
Smart play-out. OOPSLA Companion 2003: 68-69 - [c146]Amir Pnueli, Lenore D. Zuck:
Model-Checking and Abstraction to the Aid of Parameterized Systems. VMCAI 2003: 4 - [e3]Oded Maler, Amir Pnueli:
Hybrid Systems: Computation and Control, 6th International Workshop, HSCC 2003 Prague, Czech Republic, April 3-5, 2003, Proceedings. Lecture Notes in Computer Science 2623, Springer 2003, ISBN 3-540-00913-2 [contents] - 2002
- [j48]Allen Leung, Krishna V. Palem, Amir Pnueli:
TimeC: A Time Constraint Language for ILP Processor Compilation. Constraints An Int. J. 7(2): 75-115 (2002) - [j47]Amir Pnueli, Yoav Rodeh, Ofer Strichman
, Michael Siegel:
The Small Model Property: How Small Can It Be? Inf. Comput. 178(1): 279-293 (2002) - [j46]Yonit Kesten, Amir Pnueli:
Complete Proof System for QPTL. J. Log. Comput. 12(5): 701-745 (2002) - [c145]Raya Leviathan, Amir Pnueli:
Validating software pipelining optimizations. CASES 2002: 280-287 - [c144]Amir Pnueli, Jessie Xu, Lenore D. Zuck:
Liveness with (0, 1, infty)-Counter Abstraction. CAV 2002: 107-122 - [c143]Amir Pnueli, Yonit Kesten:
A Deductive Proof System for CTL. CONCUR 2002: 24-40 - [c142]Yonit Kesten, Amir Pnueli, Elad Shahar, Lenore D. Zuck:
Network Invariants in Action. CONCUR 2002: 101-115 - [c141]Amir Pnueli:
Embedded Systems: Challenges in Specification and Verification. EMSOFT 2002: 1-14 - [c140]David Harel, Hillel Kugler, Rami Marelly, Amir Pnueli:
Smart Play-out of Behavioral Requirements. FMCAD 2002: 378-398 - [c139]Werner Damm, Bernhard Josko, Amir Pnueli, Anjelika Votintseva:
Understanding UML: A Formal Semantics of Concurrency and Communication in Real-Time UML. FMCO 2002: 71-98 - [c138]Amir Pnueli:
Applications of Formal Methods in Biology. FTRTFT 2002: 81-82 - [c137]Lenore D. Zuck, Amir Pnueli, Yonit Kesten:
Automatic Verification of Probabilistic Free Choice. VMCAI 2002: 208-224 - [c136]Lenore D. Zuck, Amir Pnueli, Yi Fang, Benjamin Goldberg:
VOC: A Translation Validator for Optimizing Compilers. COCV@ETAPS 2002: 2-18 - [c135]Lenore D. Zuck, Amir Pnueli, Yi Fang, Benjamin Goldberg, Ying Hu:
Translation and Run-Time Validation of Optimized Code. RV@FLoC 2002: 179-200 - 2001
- [j45]Yonit Kesten, Amir Pnueli, Moshe Y. Vardi:
Verification by Augmented Abstraction: The Automata-Theoretic View. J. Comput. Syst. Sci. 62(4): 668-690 (2001) - [j44]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) - [j43]Allen Leung, Krishna V. Palem, Amir Pnueli:
Scheduling time-constrained instructions on pipelined processors. ACM Trans. Program. Lang. Syst. 23(1): 73-103 (2001) - [c134]Tamarah Arons, Amir Pnueli, Sitvanit Ruah, Jiazhao Xu, Lenore D. Zuck:
Parameterized Verification with Automatically Computed Inductive Assertions. CAV 2001: 221-234 - [c133]Dana Fisman
, Amir Pnueli:
Beyond Regular Model Checking. FSTTCS 2001: 156-170 - [c132]Doron A. Peled, Amir Pnueli, Lenore D. Zuck:
From Falsification to Verification. FSTTCS 2001: 292-304 - [c131]Amir Pnueli, Yoav Rodeh, Ofer Strichman:
Range Allocation for Equivalence Logic. FSTTCS 2001: 317-333 - [c130]Amir Pnueli:
Sticks and stones: a coding scheme for parameterized verification. PODC 2001: 14 - [c129]Amir Pnueli, Sitvanit Ruah, Lenore D. Zuck:
Automatic Deductive Verification with Invisible Invariants. TACAS 2001: 82-97 - 2000
- [j42]Yonit Kesten, Zohar Manna, Amir Pnueli:
Verification of Clocked and Hybrid Systems. Acta Informatica 36(11): 837-912 (2000) - [j41]Yonit Kesten, Amir Pnueli:
Verification by Augmented Finitary Abstraction. Inf. Comput. 163(1): 203-243 (2000) - [j40]Orna Lichtenstein, Amir Pnueli:
Propositional Temporal Logics: Decidability and Completeness. Log. J. IGPL 8(1): 55-85 (2000) - [j39]Eugene Asarin
, Olivier Bournez, Thao Dang, Oded Maler, Amir Pnueli:
Effective synthesis of switching controllers for linear systems. Proc. IEEE 88(7): 1011-1025 (2000) - [j38]Yonit Kesten, Amir Pnueli:
Control and Data Abstraction: The Cornerstones of Practical Formal Verification. Int. J. Softw. Tools Technol. Transf. 2(4): 328-342 (2000) - [c128]Amir Pnueli:
Rigorous development of embedded systems. CASES 2000: 1 - [c127]Amir Pnueli:
Keynote Address: Abstraction, Composition, Symmetry, and a Little Deduction: The Remedies to State Explosion. CAV 2000: 1 - [c126]Amir Pnueli, Elad Shahar:
Liveness and Acceleration in Parameterized Verification. CAV 2000: 328-343 - [c125]Ekaterina Sedletsky, Amir Pnueli, Mordechai Ben-Ari:
Formal Verification of the Ricart-Agrawala Algorithm. FSTTCS 2000: 325-335 - [c124]Tamarah Arons, Amir Pnueli:
A Comparison of Two Verification Methods for Speculative Instruction Execution. TACAS 2000: 487-502
1990 – 1999
- 1999
- [j37]Bengt Jonsson, Amir Pnueli, Camilla Rump:
Proving Refinement Using Transduction. Distributed Comput. 12(2-3): 129-149 (1999) - [j36]Yonit Kesten, Amir Pnueli, Joseph Sifakis, Sergio Yovine
:
Decidable Integration Graphs. Inf. Comput. 150(2): 209-243 (1999) - [c123]Amir Pnueli, Ofer Strichman, Michael Siegel:
Translation Validation: From SIGNAL to C. Correct System Design 1999: 231-255 - [c122]Amir Pnueli, Yoav Rodeh, Ofer Strichman, Michael Siegel:
Deciding Equality Formulas by Small Domains Instantiations. CAV 1999: 455-469 - [c121]Yonit Kesten, Amir Pnueli:
Verifying Liveness by Augmented Abstraction. CSL 1999: 141-156 - [c120]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 - [c119]Olivier Bournez, Oded Maler, Amir Pnueli:
Orthogonal Polyhedra: Representation and Computation. HSCC 1999: 46-60 - [c118]Karine Altisen, Gregor Gößler, Amir Pnueli, Joseph Sifakis, Stavros Tripakis, Sergio Yovine:
A Framework for Scheduler Synthesis. RTSS 1999: 154-163 - [c117]Tamarah Arons, Amir Pnueli:
Verifying Tomasulo's Algoithm by Refinement. VLSI Design 1999: 306-309 - 1998
- [j35]Amir Pnueli, Ofer Strichman, Michael Siegel:
The Code Validation Tool CVT: Automatic Verification of a Compilation Process. Int. J. Softw. Tools Technol. Transf. 2(2): 192-201 (1998) - [c116]