SMT 2012 Volume Information
Volume:Pascal Fontaine and Amit Goel (editors)
SMT 2012. 10th International Workshop on Satisfiability Modulo Theories

SMT 2012 Volume Information

Title:SMT 2012. 10th International Workshop on Satisfiability Modulo Theories
Editors:Pascal Fontaine and Amit Goel
Series:EPiC Series in Computing
Publication date:August 19, 2013


Armin BierePractical Aspects of SAT Solving1
Natarajan ShankarThe Architecture of Inference from SMT to ETB2
Nikolaj Bjorner, Ken McMillan and Andrey RybalchenkoProgram Verification as Satisfiability Modulo Theories3-11
Sylvain Conchon, Guillaume Melquiond, Cody Roux and Mohamed IguernelalaBuilt-in Treatment of an Axiomatic Floating-Point Theory for SMT Solvers12-21
Claire Dross, Sylvain Conchon, Johannes Kanig and Andrei PaskevichReasoning with Triggers22-31
Amit Goel, Sava Krstic, Rebekah Leslie and Mark TuttleSMT-Based System Verification with DVF32-43
Gergely Kovásznai, Andreas Fröhlich and Armin BiereOn the Complexity of Fixed-Size Bit-Vector Logics with Binary Encoded Bit-Width44-56
Mohammad Abdul Aziz, Amr Wassal and Nevin DarwishA Machine Learning Technique for Hardness Estimation of QFBV SMT Problems57-66
Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise and Natasha SharyginaReachability Modulo Theory Library67-76
Nikolaj Bjorner, Vijay Ganesh, Raphaël Michel and Margus VeanesSMT-LIB Sequences and Regular Expressions77-87
Michael Codish, Yoav Fekete, Carsten Fuhs, Jürgen Giesl and Johannes WaldmannExotic Semi-Ring Constraints88-97
Stephan Falke, Carsten Sinz and Florian MerzA Theory of Arrays with set and copy Operations98-108
Raphaël Michel, Arnaud Hubaux, Vijay Ganesh and Patrick HeymansAn SMT-based approach to automated configuration109-119
Anh-Dung Phan, Nikolaj Bjorner and David MonniauxAnatomy of Alternating Quantifier Satisfiability (Work in progress)120-130
David Cok, Alberto Griggio, Roberto Bruttomesso and Morgan DetersThe 2012 SMT Competition131-142


2decision procedure, smt lib, theories
1arithmetic, axiomatic theory, bit precise reasoning, bit vector logics, bitvectors, complexity, configuration, copy, 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 competition, smt solver, smt comp, smt evaluation, smt idl, smt lia, statistical hardness models, stp, strings, symbolic model checking, system description languages, theory of arrays, transition systems, triggers, tvl, variability, verification