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