| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Eugene Asarin, Venkatesh Mysore, Amir Pnueli, Gerardo Schneider |
Low dimensional hybrid systems - decidable, undecidable, don't know.  |
Inf. Comput.  |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Orna Kupferman, Amir Pnueli, Moshe Y. Vardi |
Once and for all. |
J. Comput. Syst. Sci. |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Ittai Balaban, Amir Pnueli, Yaniv Sa'ar, Lenore D. Zuck |
Verification of multi-linked heaps. |
J. Comput. Syst. Sci. |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Roderick Bloem, Barbara Jobstmann, Nir Piterman, Amir Pnueli, Yaniv Sa'ar |
Synthesis of Reactive(1) designs. |
J. Comput. Syst. Sci. |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Uri Klein, Nir Piterman, Amir Pnueli |
Effective Synthesis of Asynchronous Systems from GR(1) Specifications. |
VMCAI |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Amir Pnueli, Irina Virbitskaite, Andrei Voronkov (eds.) |
Perspectives of Systems Informatics, 7th International Andrei Ershov Memorial Conference, PSI 2009, Novosibirsk, Russia, June 15-19, 2009. Revised Papers |
Ershov Memorial Conference |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | Zohar Manna, Amir Pnueli |
Temporal Verification of Reactive Systems: Response. |
Essays in Memory of Amir Pnueli |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Ittai Balaban, Amir Pnueli, Lenore D. Zuck |
Proving the Refuted: Symbolic Model Checkers as Proof Generators. |
Concurrency, Compositionality, and Correctness |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Amir Pnueli, Yaniv Sa'ar, Lenore D. Zuck |
Jtlv: A Framework for Developing Verification Algorithms. |
CAV |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Uri Klein, Amir Pnueli |
Revisiting Synthesis of GR(1) Specifications. |
Haifa Verification Conference |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Amir Pnueli, Uri Klein |
Synthesis of programs from temporal property specifications. |
MEMOCODE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Hillel Kugler, Cory Plock, Amir Pnueli |
Controller Synthesis from LSC Requirements. |
FASE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Dov M. Gabbay, Amir Pnueli |
A Sound and Complete Deductive System for CTL* Verification. |
Logic Journal of the IGPL |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Amir Pnueli |
Using Abstraction to Verify Arbitrary Temporal Properties. |
APSEC |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Amir Pnueli, Aleksandr Zaks |
On the Merits of Temporal Testers. |
25 Years of Model Checking |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Anna Zaks, Amir Pnueli |
CoVaC: Compiler Validation by Program Analysis of the Cross-Product. |
FM |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Anna Zaks, Amir Pnueli |
Program analysis for compiler validation. |
PASTE |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Oded Maler, Dejan Nickovic, Amir Pnueli |
Checking Temporal Properties of Discrete, Timed and Continuous Behaviors. |
Pillars of Computer Science |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Niebert, Doron Peled, Amir Pnueli |
Discriminative Model Checking. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Ariel Cohen 0002, Amir Pnueli, Lenore D. Zuck |
Mechanical Verification of Transactional Memories with Non-transactional Memory Accesses. |
CAV |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Amir Pnueli, Yaniv Sa'ar |
All You Need Is Compassion. |
VMCAI |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Ittai Balaban, Amir Pnueli, Lenore D. Zuck |
Modular Ranking Abstraction. |
Int. J. Found. Comput. Sci. |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Roderick Bloem, Stefan J. Galler, Barbara Jobstmann, Nir Piterman, Amir Pnueli, Martin Weiglhofer |
Specify, Compile, Run: Hardware from PSL. |
Electr. Notes Theor. Comput. Sci. |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | Ariel Cohen 0002, John W. O'Leary, Amir Pnueli, Mark R. Tuttle, Lenore D. Zuck |
Verifying Correctness of Transactional Memories. |
FMCAD |
2007 |
DBLP DOI BibTeX RDF |
HTM, STM, TLC, model checking, Verification, transactional memory, TLA+ |
| 1 | Hillel Kugler, Cory Plock, Amir Pnueli |
Synthesizing reactive systems from LSC requirements using the play-engine. |
OOPSLA Companion |
2007 |
DBLP DOI BibTeX RDF |
reactive systems, live sequence charts, controller synthesis |
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | Oded Maler, Dejan Nickovic, Amir Pnueli |
On Synthesizing Controllers from Bounded-Response Properties. |
CAV |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Ittai Balaban, Amir Pnueli, Lenore D. Zuck |
Shape Analysis of Single-Parent Heaps. |
VMCAI |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Amir Pnueli, Ofer Strichman |
Reduced Functional Consistency of Uninterpreted Functions. |
Electr. Notes Theor. Comput. Sci. |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Amir Pnueli, Aleksandr Zaks, Lenore D. Zuck |
Monitoring Interfaces for Faults. |
Electr. Notes Theor. Comput. Sci. |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Yi Fang, Nir Piterman, Amir Pnueli, Lenore D. Zuck |
Liveness with invisible ranking. |
STTT |
2006 |
DBLP DOI BibTeX RDF |
Parametrized systems, Deductive verification, BDD techniques, Liveness, Automatic verification |
| 1 | Yonit Kesten, Amir Pnueli, Li-on Raviv, Elad Shahar |
Model Checking with Strong Fairness. |
Formal Methods in System Design |
2006 |
DBLP DOI BibTeX RDF |
fair discrete systems, temporal testers, model checking, temporal logic, fairness, CTL, LTL |
| 1 | Yi Fang, Kenneth L. McMillan, Amir Pnueli, Lenore D. Zuck |
Liveness by Invisible Invariants. |
FORTE |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Ittai Balaban, Amir Pnueli, Lenore D. Zuck |
Invisible Safety of Distributed Protocols. |
ICALP |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Oded Maler, Dejan Nickovic, Amir Pnueli |
From MITL to Timed Automata. |
FORMATS |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Amir Pnueli, Aleksandr Zaks |
PSL Model Checking and Run-Time Verification Via Testers. |
FM |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Nir Piterman, Amir Pnueli |
Faster Solutions of Rabin and Streett Games. |
LICS |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Nir Piterman, Amir Pnueli, Yaniv Sa'ar |
Synthesis of Reactive(1) Designs. |
VMCAI |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Ittai Balaban, Ariel Cohen 0002, Amir Pnueli |
Ranking Abstraction of Recursive Programs. |
VMCAI |
2006 |
DBLP DOI BibTeX RDF |
|
| 1 | Werner Damm, Bernhard Josko, Amir Pnueli, Angelika Votintseva |
A discrete-time UML semantics for concurrency and communication in safety-critical applications. |
Sci. Comput. Program. |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Yonit Kesten, Amir Pnueli |
A compositional approach to CTL* verification. |
Theor. Comput. Sci. |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Yonit Kesten, Nir Piterman, Amir Pnueli |
Bridging the gap between fair simulation and trace inclusion. |
Inf. Comput. |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Ying Hu, Clark W. Barrett, Benjamin Goldberg, Amir Pnueli |
Validating More Loop Optimizations. |
Electr. Notes Theor. Comput. Sci. |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
2005 |
DBLP DOI BibTeX RDF |
reordering transformations, run-time validation, speculative optimizations, global optimizations, optimizing compilers, loop transformations, translation validation, verification conditions |
| 1 | Ittai Balaban, Amir Pnueli, Lenore D. Zuck |
Ranking Abstraction as Companion to Predicate Abstraction. |
FORTE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Hillel Kugler, David Harel, Amir Pnueli, Yuan Lu, Yves Bontemps |
Temporal Logic for Scenario-Based Specifications. |
TACAS |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Amir Pnueli, Andreas Podelski, Andrey Rybalchenko |
Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete Systems. |
TACAS |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Oded Maler, Dejan Nickovic, Amir Pnueli |
Real Time Temporal Logic: Past, Present, Future. |
FORMATS |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Amir Pnueli |
Ranking Abstraction as a Companion to Predicate Abstraction, . |
ATVA |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | David Harel, Hillel Kugler, Amir Pnueli |
Synthesis Revisited: Generating Statechart Models from Scenario-Based Requirements. |
Formal Methods in Software and Systems Modeling |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Amir Pnueli |
Verification of Procedural Programs. |
We Will Show Them! |
2005 |
DBLP BibTeX RDF |
|
| 1 | Ittai Balaban, Yi Fang, Amir Pnueli, Lenore D. Zuck |
IIV: An Invisible Invariant Verifier. |
CAV |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Clark W. Barrett, Yi Fang, Benjamin Goldberg, Ying Hu, Amir Pnueli, Lenore D. Zuck |
TVOC: A Translation Validator for Optimizing Compilers. |
CAV |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Ittai Balaban, Amir Pnueli, Lenore D. Zuck |
Shape Analysis by Predicate Abstraction. |
VMCAI |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Amir Pnueli |
Abstraction for Liveness. |
VMCAI |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Venkatesh Mysore, Amir Pnueli |
Refining the Undecidability Frontier of Hybrid Automata. |
FSTTCS |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Lenore D. Zuck, Amir Pnueli |
Model checking and abstraction to the aid of parameterized systems (a survey). |
Computer Languages, Systems & Structures |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Yi Fang, Nir Piterman, Amir Pnueli, Lenore D. Zuck |
Liveness with Incomprehensible Ranking. |
TACAS |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Tamarah Arons, Jozef Hooman, Hillel Kugler, Amir Pnueli, Mark van der Zwaag |
Deductive Verification of UML Models in TLPVS. |
UML |
2004 |
DBLP DOI BibTeX RDF |
Deductive Verification, UML, Semantics, Formal Verification, Temporal Logic, State Machines, PVS |
| 1 | I. Gordin, Raya Leviathan, Amir Pnueli |
Validating the Translation of an Industrial Optimizing Compiler. |
ATVA |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Muralidhar Talupur, Nishant Sinha, Ofer Strichman, Amir Pnueli |
Range Allocation for Separation Logic. |
CAV |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | David Harel, Hillel Kugler, Amir Pnueli |
Smart Play-Out Extended: Time and Forbidden Elements. |
QSIC |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Yi Fang, Nir Piterman, Amir Pnueli, Lenore D. Zuck |
Liveness with Invisible Ranking. |
VMCAI |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | Oded Maler, Amir Pnueli |
On Recognizable Timed Languages. |
FoSSaCS |
2004 |
DBLP DOI BibTeX RDF |
|
| 1 | 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. |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Lenore D. Zuck, Amir Pnueli, Benjamin Goldberg |
VOC: A Methodology for the Translation Validation of OptimizingCompilers. |
J. UCS |
2003 |
DBLP BibTeX RDF |
|
| 1 | Michael Langberg, Amir Pnueli, Yoav Rodeh |
The ROBDD Size of Simple CNF Formulas. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | 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 |
DBLP DOI BibTeX RDF |
|
| 1 | David Harel, Hillel Kugler, Rami Marelly, Amir Pnueli |
Smart play-out. |
OOPSLA Companion |
2003 |
DBLP DOI BibTeX RDF |
play-out, system modeling and execution, UML, scenarios, object-oriented analysis and design, LSCs |
| 1 | Amir Pnueli, Tamarah Arons |
TLPVS: A PVS-Based LTL Verification System. |
Verification: Theory and Practice |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Yonit Kesten, Nir Piterman, Amir Pnueli |
Bridging the Gap between Fair Simulation and Trace Inclusion. |
CAV |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Oded Maler, Amir Pnueli (eds.) |
Hybrid Systems: Computation and Control, 6th International Workshop, HSCC 2003 Prague, Czech Republic, April 3-5, 2003, Proceedings |
|
2003 |
DBLP BibTeX RDF |
|
| 1 | Amir Pnueli, Lenore D. Zuck |
Model-Checking and Abstraction to the Aid of Parameterized Systems. |
VMCAI |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Tamarah Arons, Amir Pnueli, Lenore D. Zuck |
Parameterized Verification by Probabilistic Abstraction. |
FoSSaCS |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Allen Leung, Krishna V. Palem, Amir Pnueli |
TimeC: A Time Constraint Language for ILP Processor Compilation. |
Constraints |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Amir Pnueli, Yoav Rodeh, Ofer Strichman, Michael Siegel |
The Small Model Property: How Small Can It Be? |
Inf. Comput. |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Lenore D. Zuck, Amir Pnueli, Yi Fang, Benjamin Goldberg |
VOC: A Translation Validator for Optimizing Compilers. |
Electr. Notes Theor. Comput. Sci. |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Lenore D. Zuck, Amir Pnueli, Yi Fang, Benjamin Goldberg, Ying Hu |
Translation and Run-Time Validation of Optimized Code. |
Electr. Notes Theor. Comput. Sci. |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Yonit Kesten, Amir Pnueli |
Complete Proof System for QPTL. |
J. Log. Comput. |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Amir Pnueli, Yonit Kesten |
A Deductive Proof System for CTL. |
CONCUR |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Yonit Kesten, Amir Pnueli, Elad Shahar, Lenore D. Zuck |
Network Invariants in Action. |
CONCUR |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Amir Pnueli |
Embedded Systems: Challenges in Specification and Verification. |
EMSOFT |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | David Harel, Hillel Kugler, Rami Marelly, Amir Pnueli |
Smart Play-out of Behavioral Requirements. |
FMCAD |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Werner Damm, Bernhard Josko, Amir Pnueli, Angelika Votintseva |
Understanding UML: A Formal Semantics of Concurrency and Communication in Real-Time UML. |
FMCO |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Raya Leviathan, Amir Pnueli |
Validating software pipelining optimizations. |
CASES |
2002 |
DBLP DOI BibTeX RDF |
optimization, verification, compilers, pipeline processors, translation validation |
| 1 | Amir Pnueli, Jessie Xu, Lenore D. Zuck |
Liveness with (0, 1, infty)-Counter Abstraction. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Lenore D. Zuck, Amir Pnueli, Yonit Kesten |
Automatic Verification of Probabilistic Free Choice. |
VMCAI |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Amir Pnueli |
Applications of Formal Methods in Biology. |
FTRTFT |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Yonit Kesten, Oded Maler, Monica Marcus, Amir Pnueli, Elad Shahar |
Symbolic model checking with rich assertional languages. |
Theor. Comput. Sci. |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Allen Leung, Krishna V. Palem, Amir Pnueli |
Scheduling time-constrained instructions on pipelined processors. |
ACM Trans. Program. Lang. Syst. |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Yonit Kesten, Amir Pnueli, Moshe Y. Vardi |
Verification by Augmented Abstraction: The Automata-Theoretic View. |
J. Comput. Syst. Sci. |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Amir Pnueli, Sitvanit Ruah, Lenore D. Zuck |
Automatic Deductive Verification with Invisible Invariants. |
TACAS |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Amir Pnueli |
Sticks and stones: a coding scheme for parameterized verification. |
PODC |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Tamarah Arons, Amir Pnueli, Sitvanit Ruah, Jiazhao Xu, Lenore D. Zuck |
Parameterized Verification with Automatically Computed Inductive Assertions. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Dana Fisman, Amir Pnueli |
Beyond Regular Model Checking. |
FSTTCS |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Doron Peled, Amir Pnueli, Lenore D. Zuck |
From Falsification to Verification. |
FSTTCS |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Amir Pnueli, Yoav Rodeh, Ofer Strichman |
Range Allocation for Equivalence Logic. |
FSTTCS |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Yonit Kesten, Zohar Manna, Amir Pnueli |
Verification of Clocked and Hybrid Systems. |
Acta Inf. |
2000 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")