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 |