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.

In general, search-based solvers have been dominating symbolic solvers according to experimental results reported in the SAT and QBF literature. However, some recent efforts have contributed to close that performance gap. One novel approach involves the use of Binary Decision Diagrams(BDDs) and a simplification routine called BDD constraint propagation. The main idea is to adapt optimizations from search-based solvers in the context of BDDs. In this paper we improve upon the existing BDD constraint propagation procedure. Concretely, for a BDD A and its support set SupportSet(A), we reduce the asymptotic upper bound for the clause BDD pure literal extraction from O(A * SupportSet(A)) to O(n) time and nonclause BDD unit literal extraction from O(A * SupportSet(A)) to O(A) time. We also formulate for the first time the Trivial Falsity, Forced Literal and Universal Reduction rules for BDDs. We show in the experimental section that these improvements allow a BDD-based solver to tackle new families of problems, and outperform state-of-the art solvers in some cases.

More than any other area in computer science, the interaction and boundary between science and engineering is blurred in the systems area, with cross fertilization from both directions. The systems panel will explore the past, present and future relationship between systems research and engineering practice. They will discuss the relationship between systems research and engineering practices: when does systems innovation emanating from industry become an invention and when does academic research stop being science and become engineering? How does practice-driven research impact the real world and how does the real world reflect back on foundations? In what forms does technology create research challenges, and in what manner does applied research give solid base for development? They will surmise about the future of systems research: What are the fundamental challenges posed by the scale of today's cloud computing systems and mega-size data centers? How to organize software of large-scale distributed executions or mega-ton lines of code? What new opportunities are enabled by novel technologies like flash memory and transactional memory? How to integrate hand-in-hand design of software and architecture?

Methods in object-oriented concurrent libraries often encapsulate internal synchronization details. As a result of information hiding, clients calling the library methods may cause thread safety violations by invoking methods in an unsafe manner. This is frequently a cause of deadlocks. Given a concurrent library, we present a technique for inferring interface contracts that specify permissible concurrent method calls and patterns of aliasing among method arguments. In this work, we focus on deriving contracts that guarantee deadlock-free execution for the methods in the library. The contracts also help client developers by documenting required assumptions about the library methods. Alternatively, the contracts can be statically enforced in the client code to detect potential deadlocks in the client. Our technique combines static analysis with a symbolic encoding scheme for tracking lock dependencies, allowing us to synthesize contracts using a SMT solver. Additionally, we investigate extensions of our technique to reason about deadlocks in libraries that employ signaling primitives such as wait-notify for cooperative synchronization. Our prototype tool analyzes over a million lines of code for some widely-used Java libraries within an hour, thus demonstrating its scalability and efficiency. Furthermore, the contracts inferred by our approach have been able to pinpoint real deadlocks in clients, i.e. deadlocks that have been a part of bug-reports filed by users and developers of client code.

In this paper we present a QBF solver that is based on BDD technologies but includes optimizations from search-based algorithms. We enhance the early quantification technique from model checking, favoring aggressive quantification over conjunction of BDDs. BDD Constraint propagation is also described, a strategy inspired by the efficient simplifications applied to CNFs in DPLL-based algorithms. Some dynamic variable elimination heuristics that enforce quantification and bounded space usage are also presented, coping with the difficulties faced by static heuristics included in previous BDD-based solvers. Experimental results show that our solver outperforms both symbolic and search-based competitive solvers in formal verification benchmarks with practical applications in equivalence checking and theorem proving, by completing more problems or finishing in less time. Some preliminary results also show that the solver is able to handle some other hard problems for symbolic solvers in the planning domain with similar efficiency. The benchmarks we used contain QBFs of nearly up to 9000 variables and are available at the QBFLIB website.

We present a framework that takes unsynchronized sequential processes along with a temporal specification of their global concurrent behaviour, and automatically generates a concurrent program with synchronization code ensuring correct global behaviour. The synthesized synchronization code is based on monitors with wait and notify operations on condition variables, and mutual-exclusion locks. Novel aspects of our framework include realistic low-level synchronization implementations, synthesis of both simple coarse-grained synchronization and more complex fine-grained synchronization, and accommodation of both safety and liveness in global correctness properties. The method is fully automatic as well as sound and complete.

Model checking was introduced in the early 1980's to provide a practical automated method for verifying concurrent systems. Model checking has had substantive impact on program verification. For the first time industrial strength systems are being verified on a routine basis. As time has progressed, the term model checking has acquired slightly different shades of meaning. In this paper we these consider variant aspects of model checking, elucidating some often overlooked and subtle distinctions.

In his landmark 1977 paper "The Temporal Logic of Programs", Amir Pnueli gave a fundamental recognition that the ideally nonterminating behavior of ongoing concurrent programs, such as operating systems and protocols, was a vital aspect of program reasoning. As classical approaches to program correctness were based on initialstate/ final-state semantics for terminating programs, these approaches were inapplicable to programs where infinite behavior was the norm. To address this shortcoming, Pnueli suggested the use of temporal logic, a formalism for reasoning about change over time originally studied by philosophers, to meaningfully describe and reason about the infinite behavior of programs. This suggestion turned out to be remarkably fruitful. It struck a resonant chord within the formal verification community, and it has had an enormous impact on the development of the area. It matured into an extremely effective mathematical tool for specifying and verifying a vast class of synchronization and coordination problems common in concurrency. Pnueli thus caused a sea-change in the field of program verification, founding the time of reasoning about time, which has been the most successful period in formal methods yet.

Reliability of large-scale hardware and software systems often depends on the correctness of the underlying structured data. Examples of structured data include heap-allocated linked data structures, files, and program states in software, and netlists and simulator states for modeling hardware. In this paper, we focus on automatically transforming structured data to make it satisfy certain properties of interest. In particular, we consider tree-like structured data (i.e. trees and lists), and finite state properties of such structures (e.g. acyclicity, sorted-ness). We address two separate problems: (1) given an input structure, transforming it in a minimal fashion to obtain a desired output structure, and (2) given an input property and an output property, synthesizing a (small) update program that transforms any input satisfying the input property to some desired output. Our approach uses automata-theoretic constructions to enable efficient reasoning. The practical utility of our approach is in its ability to scale to input structures of arbitrary sizes, as illustrated by our prototype tool.

In this paper we argue that conventional mathematics word problems are not aligned with the typical learning goals and expectations partner disciplines, especially business, have in requiring that their students take mathematics courses. Using the taxonomy of educational objectives presented by Anderson and Krathwohl (2001) we show how mathematical modeling problems can be used to promote the needed alignment and contrast two examples to illustrate the differences. We then demonstrate how the more conventional word problem can be rewritten as a modeling problem. Sample assessment materials and instructional activities are included to support teachers in making the transition to the use of modeling problems.

AbstractTuring Lecture from the winners of the 2007 ACM A.M. Turing Award.In 1981, Edmund M. Clarke and E. Allen Emerson, working in the USA, and Joseph Sifakis working independently in France, authored seminal papers that founded what has become the highly successful field of model checking. This verification technology provides an algorithmic means of determining whether an abstract model---representing, for example, a hardware or software design---satisfies a formal specification expressed as a temporal logic (TL) formula. Moreover, if the property does not hold, the method identifies a counterexample execution that shows the source of the problem.The progression of model checking to the point where it can be successfully used for complex systems has required the development of sophisticated means of coping with what is known as the state explosion problem. Great strides have been made on this problem over the past 28 years by what is now a very large international research community. As a result many major hardware and software companies are beginning to use model checking in practice. Examples of its use include the verification of VLSI circuits, communication protocols, software device drivers, real-time embedded systems, and security algorithms.The work of Clarke, Emerson, and Sifakis continues to be central to the success of this research area. Their work over the years has led to the creation of new logics for specification, new verification algorithms, and surprising theoretical results. Model checking tools, created by both academic and industrial teams, have resulted in an entirely novel approach to verification and test case generation. This approach, for example, often enables engineers in the electronics industry to design complex systems with considerable assurance regarding the correctness of their initial designs. Model checking promises to have an even greater impact on the hardware and software industries in the future. ---Moshe Y. Vardi, Editor-in-Chief

Turing Lecture from the winners of the 2007 ACM A.M. Turing Award. In 1981, Edmund M. Clarke and E. Allen Emerson, working in the USA, and Joseph Sifakis working independently in France, authored seminal papers that founded what has become the highly successful field of model checking. This verification technology provides an algorithmic means of determining whether an abstract model---representing, for example, a hardware or software design---satisfies a formal specification expressed as a temporal logic (TL) formula. Moreover, if the property does not hold, the method identifies a counterexample execution that shows the source of the problem. The progression of model checking to the point where it can be successfully used for complex systems has required the development of sophisticated means of coping with what is known as the state explosion problem. Great strides have been made on this problem over the past 28 years by what is now a very large international research community. As a result many major hardware and software companies are beginning to use model checking in practice. Examples of its use include the verification of VLSI circuits, communication protocols, software device drivers, real-time embedded systems, and security algorithms. The work of Clarke, Emerson, and Sifakis continues to be central to the success of this research area. Their work over the years has led to the creation of new logics for specification, new verification algorithms, and surprising theoretical results. Model checking tools, created by both academic and industrial teams, have resulted in an entirely novel approach to verification and test case generation. This approach, for example, often enables engineers in the electronics industry to design complex systems with considerable assurance regarding the correctness of their initial designs. Model checking promises to have an even greater impact on the hardware and software industries in the future. --- Moshe Y. Vardi, Editor-in-Chief

Turing Lecture from the winners of the 2007 ACM A.M. Turing Award. In 1981, Edmund M. Clarke and E. Allen Emerson, working in the USA, and Joseph Sifakis working independently in France, authored seminal papers that founded what has become the highly successful field of model checking. This verification technology provides an algorithmic means of determining whether an abstract model---representing, for example, a hardware or software design---satisfies a formal specification expressed as a temporal logic (TL) formula. Moreover, if the property does not hold, the method identifies a counterexample execution that shows the source of the problem. The progression of model checking to the point where it can be successfully used for complex systems has required the development of sophisticated means of coping with what is known as the state explosion problem. Great strides have been made on this problem over the past 28 years by what is now a very large international research community. As a result many major hardware and software companies are beginning to use model checking in practice. Examples of its use include the verification of VLSI circuits, communication protocols, software device drivers, real-time embedded systems, and security algorithms. The work of Clarke, Emerson, and Sifakis continues to be central to the success of this research area. Their work over the years has led to the creation of new logics for specification, new verification algorithms, and surprising theoretical results. Model checking tools, created by both academic and industrial teams, have resulted in an entirely novel approach to verification and test case generation. This approach, for example, often enables engineers in the electronics industry to design complex systems with considerable assurance regarding the correctness of their initial designs. Model checking promises to have an even greater impact on the hardware and software industries in the future. --- Moshe Y. Vardi, Editor-in-Chief

Methods in object-oriented concurrent libraries hide internal synchronization details. However, information hiding may result in clients causing thread safety violations by invoking methods in an unsafe manner. Given such a library, we present a technique for inferring interface contracts that specify permissible concurrent method calls and patterns of aliasing among method arguments, such that the derived contracts guarantee deadlock free execution for the methods in the library. The contracts also help client developers by documenting required assumptions about the library methods. Alternatively, the contracts can be statically enforced in the client code to detect potential deadlocks in the client. Our technique combines static analysis with a symbolic encoding for tracking lock dependencies, allowing us to synthesize contracts using a SMT solver. Our prototype tool analyzes over a million lines of code for some widely-used Java libraries within an hour, thus demonstrating its scalability and efficiency. Furthermore, the contracts inferred by our approach have been able to pinpoint real deadlocks in clients, i.e. deadlocks that have been a part of bug-reports filed by users and developers of the client code.

Programs that manipulate heap-allocated data structures present a formidable challenge for algorithmic verification. Recursive procedures (methods) in such software libraries are used for a large number of tasks ranging from simple traversals to complex structural transformations. Verification of such methods is undecidable in general. Hence, we present a programming language fragment with a syntax similar to that of C for which correctness can be algorithmically checked. For methods written in our fragment, and specifications in the form of tree automata, verification is efficient in most cases, as illustrated by our prototype tool. Our framework can be used to verify methods such as insertion and deletion of nodes in k-ary trees, binary search trees, linked lists, linked list reversal, and rotations in balanced trees, with respect to specifications such as acyclicity, sortedness, list-ness, tree-ness, and absence of null pointer dereferences.

Automatic techniques for software verification focus on obtaining witnesses of program failure. Such counterexamples often fail to localize the precise cause of an error and usually do not suggest a repair strategy. We present an efficient algorithm to automatically generate a repair for an incorrect sequential Boolean program where program correctness is specified using a pre-condition and a post-condition. Our approach draws on standard techniques from predicate calculus to obtain annotations for the program statements. These annotations are then used to generate a synthesis query for each program statement, which if successful, yields a repair. Furthermore, we show that if a repair exists for a given program under specified conditions, our technique is always able to find it.

The first part of this two-part paper (13) described the development of a new freshman business mathematics (FBM) course at our college. In this paper, we discuss our assessment tool, the business memo, as a venue for students to apply mathematical skills, via mathematical modelling, to realistic business problems. These memos have proven a crucial step in turning our FBM course around from a dreaded course with little connection to students' intended careers into a course where students experience the power of mathematics for solving problems and informing decisions. Comments from students in the course throughout its 6-year history clearly point to the course's value and importance.

SVISS is a flexible platform for incorporating efficient symmetry reduction into symbolic model checking. The tool comes with an extensive C++ library for system modeling using BDDs and a rich CTLbased model checking engine. Applications range from communication protocols to computer hardware and multi-threaded software. We believe Sviss to be the first symbolic tool to exploit symmetry in concurrent device-driver verification, which is vital in operating system design.