Volume •Abstracts •Preface •Authors •Keywords •BibTex Entries

SMT 2012: Volume Information

SMT 2012. 10th International Workshop on Satisfiability Modulo Theories

Editors: Pascal Fontaine and Amit Goel

EPiC Series in Computing•Volume 20

15 articles•142 pages•Published: August 19, 2013

Papers

Practical Aspects of SAT Solving

1

The Architecture of Inference from SMT to ETB

Natarajan Shankar

2

Program Verification as Satisfiability Modulo Theories

Nikolaj Bjorner, Kenneth McMillan and Andrey Rybalchenko

3-11

Built-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers

Sylvain Conchon, Guillaume Melquiond, Cody Roux and Mohamed Iguernelala

12-21

Reasoning with Triggers

Claire Dross, Sylvain Conchon, Johannes Kanig and Andrei Paskevich

22-31

SMT-Based System Verification with DVF

Amit Goel, Sava Krstic, Rebekah Leslie and Mark Tuttle

32-43

On the Complexity of Fixed-Size Bit-Vector Logics with Binary Encoded Bit-Width

Gergely Kovásznai, Andreas Fröhlich and Armin Biere

44-56

A Machine Learning Technique for Hardness Estimation of QFBV SMT Problems

Mohammad Abdul Aziz, Amr Wassal and Nevine Darwish

57-66

Reachability Modulo Theory Library

Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise and Natasha Sharygina

67-76

SMT-LIB Sequences and Regular Expressions

Nikolaj Bjorner, Vijay Ganesh, Raphaël Michel and Margus Veanes

77-87

Exotic Semi-Ring Constraints

Michael Codish, Yoav Fekete, Carsten Fuhs, Jürgen Giesl and Johannes Waldmann

88-97

A Theory of Arrays with set and copy Operations

Stephan Falke, Carsten Sinz and Florian Merz

98-108

An SMT-based approach to automated configuration

Raphaël Michel, Arnaud Hubaux, Vijay Ganesh and Patrick Heymans

109-119

Anatomy of Alternating Quantifier Satisfiability (Work in progress)

Anh-Dung Phan, Nikolaj Bjørner and David Monniaux

120-130

The 2012 SMT Competition

David Cok, Alberto Griggio, Roberto Bruttomesso and Morgan Deters

131-142

Keyphrases

arithmetic, axiomatic theory, bit-precise reasoning, bit-vector logics, bitvectors, complexity, Configuration, copy, decision procedure², exotic semi-rings, floating-point, High-level modeling, Instantiation, integers, machine learning, Mapping, memcpy, memmove, memset, model checking, NEXPTIME, order encoding, Presburger arithmetic, product lines, program verification, quantifier elimination, quantifiers, Reachability Modulo Theories, real arithmetic, regular expressions, SAT encodings, satisfiability, satisfiability module theories, SET, simplex, SMT¹¹, SMT-COMP, SMT Competition, SMT-evaluation, SMT-IDL, SMT-LIA, SMT-LIB², SMT solver, Statistical Hardness models, STP, strings, symbolic model checking, system description languages, theories², Theory of Arrays, transition systems, triggers, TVL, variability, verification.