Winter 2016 — Tuesday, 2:30pm — CSE 203

Subscribe to the calendar: iCal or Google Calendar.

We’ll be reading and discussing papers relating to programming models for working with search procedures and solvers, solver technology, and reactive programming. In addition, this quarter we will also have some sessions on local work in progress, and other sessions devoted to working with different tools (solvers and languages), in which participants who are using specific tools will give informal talks/demos/code walkthroughs of the application.

Some paper links may point into the ACM Digital Library or the Springer online collection. Using a UW IP address, or the UW libraries off-campus access, should provide access. To receive announcements and news, please subscribe to the 591R mailing list.

Date	Who	What
Jan 5	Everyone	Select papers and schedule tool sessions
Jan 12	Calvin and Talia	Integrating constraint satisfaction techniques with complex object structures
Jan 19	Sam and Alex	Constraints as Control
Jan 26	Alan	Wallingford: Toward a Constraint Reactive Programming Language For background see Checks and Balances - Constraint Solving without Surprises in Object-Constraint Programming Languages
Feb 2	Pavel	Cassius
Feb 9	Eric Butler	Algebra Synthesis
Feb 16	Julian	Answer Set Programming
Feb 23	Arvind	Vega
Mar 1	Julie	Hints DSL
Mar 8	-	No meeting (Visit days)

Suggestions

Programming Models

• Constraints as Control. Ali Sinan Köksal, Viktor Kuncak, and Philippe Suter. POPL 2012

  We present an extension of Scala that supports constraint programming over bounded and unbounded domains. The resulting language, Kaplan, provides the benefits of constraint programming while preserving the existing features of Scala. Kaplan integrates constraint and imperative programming by using constraints as an advanced control structure; the developers use the monadic ’for’ construct to iterate over the solutions of constraints or branch on the existence of a solution. The constructs we introduce have simple semantics that can be understood as explicit enumeration of values, but are implemented more efficiently using symbolic reasoning.

• Integrating constraint satisfaction techniques with complex object structures. François Pachet, Pierre Roy. 15th Annual Conference of the British Computer Society Specialist Group on Expert Systems

  Integrating constraint satisfaction techniques with complex object structures is highly desirable. Several libraries are now available to use algorithms off-the shelf and embed them in large object-oriented systems. However, the design of complex object + constraint problems is an open issue that severely limits the applicability of available libraries. We compare two radically different approaches in designing systems integrating objects and finite domain constraints. In the first approach, constraints are defined within classes and constrain attributes of the class, thereby introducing “partially instantiated” objects in the reasoning. In the second approach, constraints are defined outside classes, and constrain fully instantiated objects. We show that, for a particular class of problem, the second solution yields a simpler design while being more efficient. We exemplify our claims by comparing these two approaches on a hard object + constraint problem: four-voice harmonization of tonal melodies, seen as a representative complex configuration problem

Constraint Solver Technology

• Stochastic Local Search for Satisfiability Modulo Theories Frohlich et al. AAAI 2015.

  We present a novel stochastic local search (SLS) algorithm to solve SMT problems, especially those in the theory of bit-vectors, directly on the theory level. We explain how several successful techniques used in modern SLS solvers for SAT can be lifted to the SMT level. Experimental results show that our approach can compete with state-of-the-art bit-vector solvers on many practical instances and, sometimes, outperform existing solvers. This offers interesting possibilities in combining our approach with existing techniques, and, moreover, new insights into the importance of exploiting problem structure in SLS solvers for SAT

• Impact of Community Structure on SAT Solver Performance. Zack Newsham, Vijay Ganesh, Sebastian Fischmeister, Gilles Audemard, and Laurent Simon. SAT 2015.

  Modern CDCL SAT solvers routinely solve very large industrial SAT instances in relatively short periods of time. It is clear that these solvers somehow exploit the structure of real-world instances. However, to-date there have been few results that precisely characterise this structure. In this paper, we provide evidence that the community structure of real-world SAT instances is correlated with the running time of CDCL SAT solvers.

• Are There Good Mistakes? A Theoretical Analysis of CEGIS.. Susmit Jha and Sanjit A. Seshia. SYNT 2014.

  Counterexample-guided inductive synthesis (CEGIS) is used to synthesize programs from a candidate space of programs. The technique is guaranteed to terminate and synthesize the correct program if the space of candidate programs is finite. But the technique may or may not terminate with the correct program if the candidate space of programs is infinite. In this paper, we perform a theoretical analysis of counterexample-guided inductive synthesis technique. We investigate whether the set of candidate spaces for which the correct program can be synthesized using CEGIS depends on the counterexamples used in inductive synthesis, that is, whether there are good mistakes which would increase the synthesis power. We investigate whether the use of minimal counterexamples instead of arbitrary counterexamples expands the set of candidate spaces of programs for which inductive synthesis can successfully synthesize a correct program. We consider two kinds of counterexamples: minimal counterexamples and history bounded counterexamples. The history bounded counterexample used in any iteration of CEGIS is bounded by the examples used in previous iterations of inductive synthesis. We examine the relative change in power of inductive synthesis in both cases. We show that the synthesis technique using minimal counterexamples MinCEGIS has the same synthesis power as CEGIS but the synthesis technique using history bounded counterexamples HCEGIS has different power than that of CEGIS, but none dominates the other.

• The Strategy Challenge in SMT Solving Leonardo de Moura and Grant Olney Passmore. Automated Reasoning and Mathematics, 2013.

  High-performance SMT solvers contain many tightly integrated, hand-crafted heuristic combinations of algorithmic proof methods. While these heuristic combinations tend to be highly tuned for known classes of problems, they may easily perform badly on classes of problems not anticipated by solver developers. We present a challenge to the SMT community: to develop methods through which users can exert strategic control over core heuristic aspects of SMT solvers. We present evidence that the adaptation of ideas of strategy prevalent both within the Argonne and LCF theorem proving paradigms can go a long way towards realizing this goal.

• Backdoors to Typical Case Complexity. Ryan Williams, Carla P. Gomes, and Bart Selman. IJCAI 2003.

  There has been significant recent progress in reasoning and constraint processing methods. In areas such as planning and finite model-checking, current solution techniques can handle combinatorial problems with up to a million variables and five million constraints. The good scaling behavior of these methods appears to defy what one would expect based on a worst-case complexity analysis. In order to bridge this gap between theory and practice, we propose a new framework for studying the complexity of these techniques on practical problem instances. In particular, our approach incorporates general structural properties observed in practical problem instances into the formal complexity analysis. We introduce a notion of “backdoors”, which are small sets of variables that capture the overall combinatorics of the problem instance. We provide empirical results showing the existence of such backdoors in real-world problems. We then present a series of complexity results that explain the good scaling behavior of current reasoning and constraint methods observed on practical problem instances.

• Query-Guided Maximum Satisfiability. Xin Zhang, Ravi Mangal, Aditya V. Nori, and Mayur Naik. POPL 2016.

  We propose a new optimization problem “Q-MAXSAT”, an extension of the well-known Maximum Satisfiability or MAXSAT problem. In contrast to MAXSAT, which aims to find an assignment to all variables in the formula, Q-MAXSAT computes an assignment to a desired subset of variables (or queries) in the formula. Indeed, many problems in diverse domains such as program reasoning, information retrieval, and mathematical optimization can be naturally encoded as Q-MAXSAT instances.

Reactive Programming

• Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems. Rajeev Alur, Costas Courcoubetis, Thomas A. Henzinger, and Pei-Hsin Ho.

• Practical Principled FRP. Atze van der Ploeg and Koen Claessen. (paper suggestion stolen from the 590P list)

• Asynchronous Functional Reactive Programming for GUIs. Evan Czaplicki and Stephen Chong. PLDI 2013.

Tools

Solvers

• Cassowary. Paper: The Cassowary Linear Arithmetic Constraint Solving Algorithm. Greg Badros, Alan Borning, and Peter Stuckey. Cassowary projects website: http://overconstrained.io

Languages

Applications

• A Practical Flow-Sensitive and Context-Sensitive C and C++ Memory Leak Detector. David L. Heine and Monica S. Lam. PLDI 2003.

• Static Detection of Leaks in Polymorphic Containers. David L. Heine and Monica S. Lam. ICSE 2006.

• Software Dataplane Verification. Mihai Dobrescu and Katerina Argyraki. NSDI 2014.

• Under-Constrained Symbolic Execution: Correctness Checking for Real Code. David A. Ramos and Dawson Engler. USENIX Security 2015.