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 |