In the last decade there has been a revolutionary improvement in the efficiency and expressive power of constraint solvers (e.g., SAT, SMT and CP solvers), with a consequent impact on all manner of software engineering applications and research programs. A prime example of this impact is the rapid development and adoption of solver-based symbolic-execution techniques in myriad applications such as test generation, equivalence checking, security, automated exploit construction and fault localization. Black-box use of Boolean SAT solvers for proof-of-concept has been followed by the use of Satisfiability Modulo Theories (SMT) solvers integrating rich theories to treat these applications more thoroughly. An increasing amount of work is focussing on how best to use, tune, or extend solvers to meet the needs of particular applications. A similar theme of deeper integration of solver and application can be seen with ongoing research on Constraint Programming (CP) techniques and their use in software engineering.
The workshop will focus on a broad range of topics where solvers have already made an impact, e.g., symbolic-execution based testing, as well as newer ones where their use is still nascent, e.g., testing of software product lines. The topics include, but are not limited to, the following:
Constraint-based analysis of programs and models
Constraint-based test input generation
Constraint-based exploration of programs and models
SMT and CP solvers for testing, verification, analysis, and synthesis
SMT and CP solvers and their applications in computer security
Programmable SMT and CP solvers
Combinations of constraint solvers
Constraint programming and software engineering
Solvers and software product lines
Solvers and fault localization
Following a first meeting held with the CP conference in 2006, and subsequent editions held in 2010, 2011, 2012, 2013, and 2014, and the organisation of two workshops gathering researchers from the CP and verification communities, namely CPmeetsCAV 2013 and CPmeetsVerification 2014, the aim of the CSTVA workshop at ISSTA is to bring together researchers in SAT/SMT, CP and software test/analysis in order to raise the awareness of constraint solving in the research community and encourage development of new applications and extensible solvers.
Yavuz Koroglu and Alper Sen: Design of a Modified Concolic Testing Algorithm with Smaller Constraints (Slides)
Hanefi Mercan and Cemal Yilmaz: A Constraint Solving Problem Towards Unified Combinatorial Interaction Testing
Daniel Neville, Andrew Malton, Martin Brain and Daniel Kroening: Towards Automated Bounded Model Checking of API Implementations
Session III: Concurrency Chair: Vijay Ganesh
Murali Krishna Ramanathan: Leveraging Constraint Solvers in Building Reliable Multithreaded Software
Allan Blanchard, Nikolai Kosmatov and Frédéric Loulergue: A CHR-Based Solver for Weak Memory Behaviors
Open discussion Moderator: Christoph M. Wintersteiger
We invite three categories of submissions:
Research papers: Original contributions, presenting novel ideas, results or systems in constraint-based software engineering. Papers should not be published or submitted elsewhere during the time of evaluation.
Tool demonstrations, short papers & fast abstracts: Propose tool demonstrations, brief notes, or abstracts, presenting new tools, new challenges or groundbreaking results in constraint-based software engineering.
Presentation-only papers: describe work recently published or submitted elsewhere and will not be included in the proceedings. We see this as a way to provide additional access to important developments that CSTVA attendees may be unaware of. If accepted, papers in this category cannot be promoted to another category.