Search

Your search keyword '"Emerson, E. Allen"' showing total 350 results
Start Over Author "Emerson, E. Allen"

Refine your results

more »

more »

more »

more »
350 results on '"Emerson, E. Allen"'

2. Cost-Aware Automatic Program Repair

Author

Samanta, Roopsha, Olivo, Oswaldo, and Emerson, E. Allen

Subjects
Computer Science - Programming Languages
Abstract

We present a formal framework for repairing infinite-state, imperative, sequential programs, with (possibly recursive) procedures and multiple assertions; the framework can generate repaired programs by modifying the original erroneous program in multiple program locations, and can ensure the readability of the repaired program using user-defined expression templates; the framework also generates a set of inductive assertions that serve as a proof of correctness of the repaired program. As a step toward integrating programmer intent and intuition in automated program repair, we present a " cost-aware" formulation - given a cost function associated with permissible statement modifications, the goal is to ensure that the total program modification cost does not exceed a given repair budget. As part of our predicate abstraction-based solution framework, we present a sound and complete algorithm for repair of Boolean programs. We have developed a prototype tool based on SMT solving and used it successfully to repair diverse errors in benchmark C programs.

Published
2013

3. Cost-Aware Automatic Program Repair

Author

Samanta, Roopsha, Olivo, Oswaldo, Emerson, E. Allen, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Kobsa, Alfred, Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Weikum, Gerhard, Series editor, Müller-Olm, Markus, editor, and Seidl, Helmut, editor

Published
2014
Full Text
View/download PDF

4. An Algorithmic Framework for Synthesis of Concurrent Programs

Author

Emerson, E. Allen, Samanta, Roopsha, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Bultan, Tevfik, editor, and Hsiung, Pao-Ann, editor

Published
2011
Full Text
View/download PDF

5. A More Efficient BDD-Based QBF Solver

Author

Olivo, Oswaldo, Emerson, E. Allen, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, and Lee, Jimmy, editor

Published
2011
Full Text
View/download PDF

6. Meanings of Model Checking

Author

Emerson, E. Allen, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Doug, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Dams, Dennis, editor, Hannemann, Ulrich, editor, and Steffen, Martin, editor

Published
2010
Full Text
View/download PDF

7. The Beginning of Model Checking: A Personal Perspective

Author

Emerson, E. Allen, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Grumberg, Orna, editor, and Veith, Helmut, editor

Published
2008
Full Text
View/download PDF

8. DESIGN AND SYNTHESIS OF SYNCHRONIZATION SKELETONS USING BRANCHING TIME TEMPORAL LOGIC

Author

Clarke, Edmund M., Emerson, E. Allen, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Grumberg, Orna, editor, and Veith, Helmut, editor

Published
2008
Full Text
View/download PDF

9. SVISS: Symbolic Verification of Symmetric Systems

Author

Wahl, Thomas, Blanc, Nicolas, Emerson, E. Allen, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Doug, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Ramakrishnan, C. R., editor, and Rehof, Jakob, editor

Published
2008
Full Text
View/download PDF

10. Reducing Model Checking of the Few to the One

Author

Emerson, E. Allen, Trefler, Richard J., Wahl, Thomas, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Liu, Zhiming, editor, and He, Jifeng, editor

Published
2006
Full Text
View/download PDF

11. Automatic Verification of Parameterized Data Structures

Author

Deshmukh, Jyotirmoy V., Emerson, E. Allen, Gupta, Prateek, Hutchison, David, Series editor, Kanade, Takeo, Series editor, Kittler, Josef, Series editor, Kleinberg, Jon M., Series editor, Mattern, Friedemann, Series editor, Mitchell, John C., Series editor, Naor, Moni, Series editor, Nierstrasz, Oscar, Series editor, Pandu Rangan, C., Series editor, Steffen, Bernhard, Series editor, Sudan, Madhu, Series editor, Terzopoulos, Demetri, Series editor, Tygar, Dough, Series editor, Vardi, Moshe Y., Series editor, Weikum, Gerhard, Series editor, Hermanns, Holger, editor, and Palsberg, Jens, editor

Published
2006
Full Text
View/download PDF

12. Predictive Reachability Using a Sample-Based Approach

Author

Sahoo, Debashis, Jain, Jawahar, Iyer, Subramanian K., Dill, David, Emerson, E. Allen, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Borrione, Dominique, editor, and Paul, Wolfgang, editor

Published
2005
Full Text
View/download PDF

13. Dynamic Symmetry Reduction

Author

Emerson, E. Allen, Wahl, Thomas, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Halbwachs, Nicolas, editor, and Zuck, Lenore D., editor

Published
2005
Full Text
View/download PDF

14. On Partitioning and Symbolic Model Checking

Author

Iyer, Subramanian, Sahoo, Debashis, Emerson, E. Allen, Jain, Jawahar, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Fitzgerald, John, editor, Hayes, Ian J., editor, and Tarlecki, Andrzej, editor

Published
2005
Full Text
View/download PDF

15. A Partitioning Methodology for BDD-Based Verification

Author

Sahoo, Debashis, Iyer, Subramanian, Jain, Jawahar, Stangier, Christian, Narayan, Amit, Dill, David L., Emerson, E. Allen, Hutchison, David, editor, Kanade, Takeo, editor, Kittler, Josef, editor, Kleinberg, Jon M., editor, Mattern, Friedemann, editor, Mitchell, John C., editor, Naor, Moni, editor, Nierstrasz, Oscar, editor, Pandu Rangan, C., editor, Steffen, Bernhard, editor, Sudan, Madhu, editor, Terzopoulos, Demetri, editor, Tygar, Dough, editor, Vardi, Moshe Y., editor, Weikum, Gerhard, editor, Hu, Alan J., editor, and Martin, Andrew K., editor

Published
2004
Full Text
View/download PDF

26. Model Checking Synchronous Timing Diagrams

Author

Amla, Nina, Emerson, E. Allen, Kurshan, Robert P., Namjoshi, Kedar S., Goos, Gerhard, editor, Hartmanis, Juris, editor, van Leeuwen, Jan, editor, Hunt, Warren A., Jr., editor, and Johnson, Steven D., editor

Published
2000
Full Text
View/download PDF

38. Quantitative temporal reasoning

Author

Emerson, E. Allen, Mok, A. K., Sistla, A. P., Srinivasan, Jai, Goos, Gerhard, editor, Hartmanis, Juris, editor, Clarke, Edmund M., editor, and Kurshan, Robert P., editor

Published
1991
Full Text
View/download PDF

43. On partitioning and symbolic model checking

Author

Iyer, Subramanian, Sahoo, Debashis, Emerson, E. Allen, and Jain, Jawahar

Subjects
Decision tree -- Analysis, Binary-coded notation -- Analysis, Image processing -- Analysis
Published
2006

44. Synthesis of fault-tolerant concurrent programs

Author

Attie, Paul C., Arora, Anish, and Emerson, E. Allen

Subjects
Programming language, Programming languages -- Research
Abstract

Methods for mechanically synthesizing concurrent programs from temporal logic specifications obviate the need to manually construct a program and compose a proof of its correctness. A serious drawback of extant synthesis methods, however, is that they produce concurrent programs for models of computation that are often unrealistic. In particular, these methods assume completely fault-free operation, that is, the programs they produce are fault-intolerant. In this paper, we show how to mechanically synthesize fault-tolerant concurrent programs for various fault classes. We illustrate our method by synthesizing fault-tolerant solutions to the mutual exclusion and barrier synchronization problems. Categories and Subject Descriptors: C.2.4 [Computer-Communication Networks]: Distributed Systems; C.4 [Performance of Systems]: Fault Tolerance; D. 1.2 [Programming Techniques]: Automatic Programming; D.1.3 [Programming Techniques]: Concurrent Programming; D.2.2 [Software Engineering]: Design Tools and Techniques--State diagrams; D.2.4 [Software Engineering]: Software/Program Verification--Correctness proofs, formal methods, model checking, reliability; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs--Logics of programs, mechanical verification, specification techniques; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic--Temporal logic; 1.2.2 [Artificial Intelligence]: Automatic Programming--Program synthesis

Published
2004

50. Synthesis of current programs for an atomic read/write model of computation

Author

Attie, Paul C. and Emerson, E. Allen

Subjects
Computer programming, Parallel processing, Computer programming -- Methods -- Models, Concurrent programming -- Models -- Methods, Parallel processing -- Models -- Methods, Multitasking -- Models -- Methods
Abstract

1. INTRODUCTION Methods for synthesizing (finite state) concurrent programs from temporal logic specifications based on the use of a decision procedure for testing temporal satisfiability have been proposed by Emerson […], Methods for mechanically synthesizing concurrent programs from temporal logic specifications have been proposed by Emerson and Clarke and by Manna and Wolper. An important advantage of these synthesis methods is that they obviate the need to manually compose a program and manually construct a proof of its correctness. A serious drawback of these methods in practice, however, is that they produce concurrent programs for models of computation that are often unrealistic, involving highly centralized system architecture (Manna and Wolper), processes with global information about the system state (Emerson and Clarke), or reactive modules that can read all of their inputs in one atomic step (Anuchitanukul and Manna, and Pnueli and Rosner). Even simple synchronization protocols based on atomic read/write primitives such as Peterson's solution to the mutual exclusion problem have remained outside the scope of practical mechanical synthesis methods. In this paper, we show how to mechanically synthesize in more realistic computational models solutions to synchronization problems. We illustrate the method by synthesizing Peterson's solution to the mutual exclusion problem. Categories and Subject Descriptors: C.2.4 [Computer-Communication Networks]: Distributed Systems; D. 1.2 [Programming Techniques]: Automatic Programming; D. 1.3 [Programming Techniques]: Concurrent Programming; D.2.1 [Software Engineering]: Requirements/ Specifications; D.2.2 [Software Engineering]: Design Tools and Techniques--state diagrams; D.2.4 [Software Engineering]: Software/Program Verification--correctness proofs, formal methods, model checking; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs--logics of programs, mechanical verification; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic--temporal logic; 1.2.2 [Artificial Intelligence]: Automatic Programming--program synthesis General Terms: Design, Languages, Theory, Verification Additional Key Words and Phrases: Atomic registers, concurrent programs, program synthesis, specification, temporal logic

Published
2001

Catalog

Books, media, physical & digital resources
See catalog results