Amir Pnueli - researchr profile publications

researchr

You are not signed in
Sign in
Sign up

2009

Controller Synthesis from LSC RequirementsHillel Kugler, Cory Plock, Amir Pnueli. FASE 2009: 79-93 [doi]

2008

Mechanical Verification of Transactional Memories with Non-transactional Memory AccessesAriel Cohen 0002, Amir Pnueli, Lenore D. Zuck. cav 2008: 121-134 [doi]

A Sound and Complete Deductive System for CTL* VerificationDov M. Gabbay, Amir Pnueli. igpl, 16(6):499-536, 2008. [doi]

Checking Temporal Properties of Discrete, Timed and Continuous BehaviorsOded Maler, Dejan Nickovic, Amir Pnueli. birthday 2008: 475-505 [doi]

Discriminative Model CheckingPeter Niebert, Doron Peled, Amir Pnueli. cav 2008: 504-516 [doi]

On the Merits of Temporal TestersAmir Pnueli, Aleksandr Zaks. spin 2008: 172-195 [doi]

All You Need Is CompassionAmir Pnueli, Yaniv Sa ar. vmcai 2008: 233-247 [doi]

Using Abstraction to Verify Arbitrary Temporal PropertiesAmir Pnueli. apsec 2008: 3 [doi]

CoVaC: Compiler Validation by Program Analysis of the Cross-ProductAnna Zaks, Amir Pnueli. fm 2008: 35-51 [doi]

Program analysis for compiler validationAnna Zaks, Amir Pnueli. PASTE 2008: 1-7 [doi]

2007

Verifying Correctness of Transactional MemoriesAriel Cohen 0002, John W. O Leary, Amir Pnueli, Mark R. Tuttle, Lenore D. Zuck. FMCAD 2007: 37-44 [doi]

Modular Ranking AbstractionIttai Balaban, Amir Pnueli, Lenore D. Zuck. ijfcs, 18(1):5-44, 2007. [doi]

Shape Analysis of Single-Parent HeapsIttai Balaban, Amir Pnueli, Lenore D. Zuck. vmcai 2007: 91-105 [doi]

Specify, Compile, Run: Hardware from PSLRoderick Bloem, Stefan Galler, Barbara Jobstmann, Nir Piterman, Amir Pnueli, Martin Weiglhofer. ENTCS, 190(4):3-16, 2007. [doi]

Interactive presentation: Automatic hardware synthesis from specifications: a case studyRoderick Bloem, Stefan Galler, Barbara Jobstmann, Nir Piterman, Amir Pnueli, Martin Weiglhofer. date 2007: 1188-1193 [doi]

Synthesizing reactive systems from LSC requirements using the play-engineHillel Kugler, Cory Plock, Amir Pnueli. OOPSLA 2007: 801-802 [doi]

Don t Care Modeling: A Logical Framework for Developing Predictive System ModelsHillel Kugler, Amir Pnueli, Michael J. Stern, E. Jane Albert Hubbard. TACAS 2007: 343-357 [doi]

On Synthesizing Controllers from Bounded-Response PropertiesOded Maler, Dejan Nickovic, Amir Pnueli. cav 2007: 95-107 [doi]

2006

Ranking Abstraction of Recursive ProgramsIttai Balaban, Ariel Cohen 0002, Amir Pnueli. vmcai 2006: 267-281 [doi]

Invisible Safety of Distributed ProtocolsIttai Balaban, Amir Pnueli, Lenore D. Zuck. icalp 2006: 528-539 [doi]

Liveness by Invisible InvariantsYi Fang, Kenneth L. McMillan, Amir Pnueli, Lenore D. Zuck. forte 2006: 356-371 [doi]

Liveness with invisible rankingYi Fang, Nir Piterman, Amir Pnueli, Lenore D. Zuck. STTT, 8(3):261-279, 2006. [doi]

Model Checking with Strong FairnessYonit Kesten, Amir Pnueli, Li-on Raviv, Elad Shahar. fmsd, 28(1):57-84, 2006. [doi]

From MITL to Timed AutomataOded Maler, Dejan Nickovic, Amir Pnueli. formats 2006: 274-289 [doi]

Faster Solutions of Rabin and Streett GamesNir Piterman, Amir Pnueli. lics 2006: 275-284 [doi]

Synthesis of Reactive(1) DesignsNir Piterman, Amir Pnueli, Yaniv Sa ar. vmcai 2006: 364-380 [doi]

Monitoring Interfaces for FaultsAmir Pnueli, Aleksandr Zaks, Lenore D. Zuck. ENTCS, 144(4):73-89, 2006. [doi]

Reduced Functional Consistency of Uninterpreted FunctionsAmir Pnueli, Ofer Strichman. ENTCS, 144(2):53-65, 2006. [doi]

PSL Model Checking and Run-Time Verification Via TestersAmir Pnueli, Aleksandr Zaks. fm 2006: 573-586 [doi]

2005

IIV: An Invisible Invariant VerifierIttai Balaban, Yi Fang, Amir Pnueli, Lenore D. Zuck. cav 2005: 408-412 [doi]

Ranking Abstraction as Companion to Predicate AbstractionIttai Balaban, Amir Pnueli, Lenore D. Zuck. forte 2005: 1-12 [doi]

Shape Analysis by Predicate AbstractionIttai Balaban, Amir Pnueli, Lenore D. Zuck. vmcai 2005: 164-180 [doi]

TVOC: A Translation Validator for Optimizing CompilersClark W. Barrett, Yi Fang, Benjamin Goldberg, Ying Hu, Amir Pnueli, Lenore D. Zuck. cav 2005: 291-295 [doi]

A discrete-time UML semantics for concurrency and communication in safety-critical applicationsWerner Damm, Bernhard Josko, Amir Pnueli, Angelika Votintseva. SCP, 55(1-3):81-115, 2005. [doi]

Synthesis Revisited: Generating Statechart Models from Scenario-Based RequirementsDavid Harel, Hillel Kugler, Amir Pnueli. BIRTHDAY 2005: 309-324 [doi]

Validating More Loop OptimizationsYing Hu, Clark W. Barrett, Benjamin Goldberg, Amir Pnueli. ENTCS, 141(2):69-84, 2005. [doi]

Bridging the gap between fair simulation and trace inclusionYonit Kesten, Nir Piterman, Amir Pnueli. iandc, 200(1):35-61, 2005. [doi]

A compositional approach to CTL* verificationYonit Kesten, Amir Pnueli. TCS, 331(2-3):397-428, 2005. [doi]

Temporal Logic for Scenario-Based SpecificationsHillel Kugler, David Harel, Amir Pnueli, Yuan Lu, Yves Bontemps. TACAS 2005: 445-460 [doi]

Real Time Temporal Logic: Past, Present, FutureOded Maler, Dejan Nickovic, Amir Pnueli. formats 2005: 2-16 [doi]

Refining the Undecidability Frontier of Hybrid AutomataVenkatesh Mysore, Amir Pnueli. fsttcs 2005: 261-272 [doi]

Verification of Procedural ProgramsAmir Pnueli. BIRTHDAY 2005: 543-590

Ranking Abstraction as a Companion to Predicate Abstraction, Amir Pnueli. ATVA 2005: 1 [doi]

Abstraction for LivenessAmir Pnueli. vmcai 2005: 146-146 [doi]

Separating Fairness and Well-Foundedness for the Analysis of Fair Discrete SystemsAmir Pnueli, Andreas Podelski, Andrey Rybalchenko. TACAS 2005: 124-139 [doi]

Translation and Run-Time Validation of Loop TransformationsLenore D. Zuck, Amir Pnueli, Benjamin Goldberg, Clark W. Barrett, Yi Fang, Ying Hu. fmsd, 27(3):335-360, 2005. [doi]

2004

Deductive Verification of UML Models in TLPVSTamarah Arons, Jozef Hooman, Hillel Kugler, Amir Pnueli, Mark van der Zwaag. uml 2004: 335-349 [doi]

Liveness with Incomprehensible RankingYi Fang, Nir Piterman, Amir Pnueli, Lenore D. Zuck. TACAS 2004: 482-496 [doi]

Liveness with Invisible RankingYi Fang, Nir Piterman, Amir Pnueli, Lenore D. Zuck. vmcai 2004: 223-238 [doi]

Validating the Translation of an Industrial Optimizing CompilerI. Gordin, Raya Leviathan, Amir Pnueli. ATVA 2004: 230-247 [doi]

Smart Play-Out Extended: Time and Forbidden ElementsDavid Harel, Hillel Kugler, Amir Pnueli. qsic 2004: 2-10 [doi]

On Recognizable Timed LanguagesOded Maler, Amir Pnueli. fossacs 2004: 348-362 [doi]

Range Allocation for Separation LogicMuralidhar Talupur, Nishant Sinha, Ofer Strichman, Amir Pnueli. cav 2004: 148-161 [doi]

Model checking and abstraction to the aid of parameterized systems (a survey)Lenore D. Zuck, Amir Pnueli. Comp. Lang., Syst. \& Struct., 30(3-4):139-169, 2004. [doi]

2003

Formal Modeling of C. elegans Development: A Scenario-Based ApproachNa aman Kam, David Harel, Hillel Kugler, Rami Marelly, Amir Pnueli, E. Jane Albert Hubbard, Michael J. Stern. cmsb 2003: 4-20 [doi]

Parameterized Verification by Probabilistic AbstractionTamarah Arons, Amir Pnueli, Lenore D. Zuck. fossacs 2003: 87-102 [doi]

Smart play-outDavid Harel, Hillel Kugler, Rami Marelly, Amir Pnueli. OOPSLA 2003: 68-69 [doi]

Bridging the Gap between Fair Simulation and Trace InclusionYonit Kesten, Nir Piterman, Amir Pnueli. cav 2003: 381-393 [doi]

The ROBDD Size of Simple CNF FormulasMichael Langberg, Amir Pnueli, Yoav Rodeh. charme 2003: 363-377 [doi]

Hybrid Systems: Computation and Control, 6th International Workshop, HSCC 2003 Prague, Czech Republic, April 3-5, 2003, ProceedingsOded Maler, Amir Pnueli, editors, Volume 2623 of Lecture Notes in Computer Science, Springer, 2003.

Erratum ( The small model property: how small can it be? Volume 178, Number 1 [2002], pages 279-293)Amir Pnueli, Yoav Rodeh, Ofer Strichman, Michael Siegel. iandc, 184(1):227, 2003. [doi]

TLPVS: A PVS-Based LTL Verification SystemAmir Pnueli, Tamarah Arons. BIRTHDAY 2003: 598-625 [doi]

Model-Checking and Abstraction to the Aid of Parameterized SystemsAmir Pnueli, Lenore D. Zuck. vmcai 2003: 4 [doi]

VOC: A Methodology for the Translation Validation of OptimizingCompilersLenore D. Zuck, Amir Pnueli, Benjamin Goldberg. jucs, 9(3):223-247, 2003. [doi]

2002

Understanding UML: A Formal Semantics of Concurrency and Communication in Real-Time UMLWerner Damm, Bernhard Josko, Amir Pnueli, Angelika Votintseva. FMCO 2003: 71-98 [doi]

Smart Play-out of Behavioral RequirementsDavid Harel, Hillel Kugler, Rami Marelly, Amir Pnueli. FMCAD 2002: 378-398 [doi]

Network Invariants in ActionYonit Kesten, Amir Pnueli, Elad Shahar, Lenore D. Zuck. concur 2002: 101-115 [doi]

Complete Proof System for QPTLYonit Kesten, Amir Pnueli. logcom, 12(5):701-745, 2002. [doi]

TimeC: A Time Constraint Language for ILP Processor CompilationAllen Leung, Krishna V. Palem, Amir Pnueli. constraints, 7(2):75-115, 2002.

Validating software pipelining optimizationsRaya Leviathan, Amir Pnueli. cases 2002: 280-287 [doi]

The Small Model Property: How Small Can It Be?Amir Pnueli, Yoav Rodeh, Ofer Strichman, Michael Siegel. iandc, 178(1):279-293, 2002. [doi]

A Deductive Proof System for CTLAmir Pnueli, Yonit Kesten. concur 2002: 24-40 [doi]

Embedded Systems: Challenges in Specification and VerificationAmir Pnueli. emsoft 2002: 1-14 [doi]

Applications of Formal Methods in BiologyAmir Pnueli. ftrtft 2002: 81-82 [doi]

Liveness with (0, 1, infty)-Counter AbstractionAmir Pnueli, Jessie Xu, Lenore D. Zuck. cav 2002: 107-122 [doi]

Automatic Verification of Probabilistic Free ChoiceLenore D. Zuck, Amir Pnueli, Yonit Kesten. vmcai 2002: 208-224 [doi]

VOC: A Translation Validator for Optimizing CompilersLenore D. Zuck, Amir Pnueli, Yi Fang, Benjamin Goldberg. ENTCS, 65(2), 2002. [doi]

2001

Parameterized Verification with Automatically Computed Inductive AssertionsTamarah Arons, Amir Pnueli, Sitvanit Ruah, Jiazhao Xu, Lenore D. Zuck. cav 2001: 221-234 [doi]

Beyond Regular Model CheckingDana Fisman, Amir Pnueli. fsttcs 2001: 156-170 [doi]

Verification by Augmented Abstraction: The Automata-Theoretic ViewYonit Kesten, Amir Pnueli, Moshe Y. Vardi. jcss, 62(4):668-690, 2001.

Symbolic model checking with rich assertional languagesYonit Kesten, Oded Maler, Monica Marcus, Amir Pnueli, Elad Shahar. TCS, 256(1-2):93-112, 2001. [doi]

Scheduling time-constrained instructions on pipelined processorsAllen Leung, Krishna V. Palem, Amir Pnueli. TOPLAS, 23(1):73-103, 2001. [doi]

From Falsification to VerificationDoron Peled, Amir Pnueli, Lenore D. Zuck. fsttcs 2001: 292-304 [doi]

Automatic Deductive Verification with Invisible InvariantsAmir Pnueli, Sitvanit Ruah, Lenore D. Zuck. TACAS 2001: 82-97 [doi]

Sticks and stones: a coding scheme for parameterized verificationAmir Pnueli. podc 2001: 14 [doi]

Range Allocation for Equivalence LogicAmir Pnueli, Yoav Rodeh, Ofer Strichman. fsttcs 2001: 317-333 [doi]

2000

A Comparison of Two Verification Methods for Speculative Instruction ExecutionTamarah Arons, Amir Pnueli. TACAS 2000: 487-502 [doi]

Verification of Clocked and Hybrid SystemsYonit Kesten, Zohar Manna, Amir Pnueli. ACTA, 36(11):837-912, 2000. [doi]

Verification by Augmented Finitary AbstractionYonit Kesten, Amir Pnueli. iandc, 163(1):203-243, 2000.

Control and Data Abstraction: The Cornerstones of Practical Formal VerificationYonit Kesten, Amir Pnueli. STTT, 2(4):328-342, 2000. [doi]

Propositional Temporal Logics: Decidability and CompletenessOrna Lichtenstein, Amir Pnueli. igpl, 8(1), 2000. [doi]

Liveness and Acceleration in Parameterized VerificationAmir Pnueli, Elad Shahar. cav 2000: 328-343

Rigorous development of embedded systemsAmir Pnueli. cases 2000: 1 [doi]

Keynote Address: Abstraction, Composition, Symmetry, and a Little Deduction: The Remedies to State ExplosionAmir Pnueli. cav 2000: 1

Formal Verification of the Ricart-Agrawala AlgorithmEkaterina Sedletsky, Amir Pnueli, Mordechai Ben-Ari. fsttcs 2000: 325-335 [doi]

1999

PreviousNext