 |
10 elements available |  | |  | | | | | Date: | 03-Feb-2012 | | Title: | SMT Workshop 2012
| | Hits: | 228 | | Contributed by: | Roberto Bruttomesso | | Keywords: | Satisfiability Modulo Theory, SAT/CP Integration, null, null, null, null, null, null, null, null, null, null |
| | | |  |  | |
| |
======================================================================
SMT Workshop 2012
10th International Workshop on Satisfiability Modulo Theories
Affiliated with IJCAR’2012, Manchester, UK
June 30th - July 1st, 2012
Collocated with The Alan Turing Centenary Conference
http://smt2012.loria.fr
---CALL FOR PAPERS---
======================================================================
Background
----------
Determining the satisfiability of first-order formulas modulo
background theories, known as the Satisfiability Modulo Theories (SMT)
problem, has proved to be an enabling technology for verification,
synthesis, test generation, compiler optimization, scheduling, and
other areas. The success of SMT techniques depends on the development
of both domain-specific decision procedures for each background theory
(e.g., linear arithmetic, the theory of arrays, or the theory of
bit-vectors) and combination methods that allow one to obtain more
versatile SMT tools, usually leveraging Boolean satisfiability (SAT)
solvers. These ingredients together make SMT techniques well-suited
for use in larger automated reasoning and verification efforts.
Aims and Scope
--------------
The aim of the workshop is to bring together researchers and users of
SMT tools and techniques. Relevant topics include but are not limited to:
* Decision procedures and theories of interest
* Combinations of decision procedures
* Novel implementation techniques
* Benchmarks and evaluation methodologies
* Applications and case studies
* Theoretical results
Papers on pragmatic aspects of implementing and using SMT tools, as well
as novel applications of SMT, are especially encouraged.
Important dates
---------------
* Submission deadline - April 16th, 2012
* Notification - May 7th, 2012
* Camera ready versions due - May 28th, 2012
* Workshop - June 30th and July 1st, 2012
Paper submission and Proceedings
--------------------------------
Three categories of submissions are invited:
* Extended abstracts: given the informal style of the workshop, we
strongly encourage the submission of preliminary reports of work in
progress. They may range in length from very short (a couple of
pages) to the full 10 pages and they will be judged based on the
expected level of interest for the SMT community. They will be
included in the informal proceedings.
* Original papers: contain original research (simultaneous submissions
are not allowed) and sufficient detail to assess the merits and
relevance of the submission. For papers reporting experimental
results, authors are strongly encouraged to make their data
available.
* Presentation-only papers: describe work recently published or
submitted and will not be included in the proceedings. We see this
as a way to provide additional access to important developments that
SMT Workshop attendees may be unaware of.
Papers in all three categories will be peer-reviewed. Papers should
not exceed 10 pages (Postscript or PDF) and should be in
standard-conforming Postscript or PDF. Technical details may be
included in an appendix to be read at the reviewers' discretion.
Final versions should be prepared in LaTeX using the easychair.cls
class file.
To submit a paper, go to the EasyChair SMT page
http://www.easychair.org/conferences/?conf=smt2012 and follow the
instructions there.
|
| |  | |  |
| | |
| | | | | | | | Date: | 24-Jan-2011 | | Title: | Aalto University: Three tenure track positions in information and computer science
| | Hits: | 701 | | Contributed by: | Ilkka Niemela | | Keywords: | Complexity, SAT application, Logic, Linear Programming, Non-monotonic reasoning, Satisfiability Modulo Theory, Constraint Programming, null, null, null, null |
| | | | | | |
| | | Aalto University School of Science (Helsinki, Finland) invites applications for three tenured of tenure track positions in the Department of Information and Computer Science (http://ics.tkk.fi/en/) open to outstanding individuals who hold a doctorate and have excellent potential for a successful scientific career.
Closing Date for Applications: 2011-02-04
For more details, see http://dept.ics.tkk.fi/calls/tenuretrack2011/ |
| | | | |
| | |
| | | | | | | | Date: | 03-Nov-2010 | | Title: | Yves Crama and Peter L. Hammer (eds), Boolean Models and Methods in Mathematics, Computer Science, and Engineering, Cambridge University Press, 2010
| | Hits: | 1029 | | Contributed by: | Crama Yves | | Keywords: | Deduction Rules, BDD, Random 3SAT, Complexity, Computational logic, SAT application, Randomised Algorithms, Randomised Problem Generation, Learning, Logic, phase transition, resolution complexity, Linear Programming, MAXSAT, Unit Propagation, General Interest, Boolean functions, Resolution proof, null, null, null, null, null, null |
| | | | | | |
| | |
| |
This thesis is proposed by ONERA's information processing and systems modelling department in Toulouse, France, in partneship with Rockwell
Collins France (French subsidiary of Rockwell Collins Inc.), a leading
designer and provider of critical aerospace systems, enjoying a
internationally renowned expertise in formal methods.
Critical systems and software are subject to diverse and drastic
requirements such as functional correctness under hard real-time
constraints, fault-tolerance constraints, reconfiguration constraints,
etc. Over the years, a range of model driven engineering techniques
and formal analysis methods and techniques were developed
(scheduling analysis, real-time performance prediction, automatic
bug finding, automatic proof of absence of bug, …) and refined to
reach a high maturity.
Despite these continuous advances in formal methods, users often
experience technical difficulties in scaling up formal methods to
models of real world systems, either because of their important size,
because or because of their inherent computational complexity (when
they make use of non linear integer arithmetic, or floating point
arithmetic for instance). Methodological and process issues can also
come in the way, but this thesis will be primarily focused on the
technical side of the problem.
Nevertheless, it seems some progress can be achieved on these
technical issues by establishing a tight cooperation between different
and mature approaches to formal verification.
In particular, SMT-based temporal model checking techniques (MC),
which allow to verify safety and liveness properties on transition
systems, have gained momentum thanks to the recent and dramatic
advances in SMT solvers performance, invariant strengthening for k-induction based techniques and Craig interpolant generation techniques for heterogeneous logics. Still,
proofs can fail, and extra non-trivial information (i.e. lemmas) often
has to be manually added to a model to allow a proof to be obtained.
Similarly, abstract interpretation (AI) techniques have become
extremely effective, but are somehow dedicated to the analysis of
predefined property patterns on imperative code, such as out of bounds
accesses in arrays, integer overflows/underflows, or to finding bounds
on the error between an ideal computation using real numbers and its
implementation using floating point numbers.
The Ph.D. student will have to study in which way these two families
of techniques (MC/AI) can complement each other so as to overcome
their own limitations, hopefully extending the range of critical
aerospace systems that can be addressed with formal methods.
Full details and contact information available in this
ONERA PDF document
The thesis will follow a CIFRE convention (Click for CIFRE financing information) |
| | | | |
| | |
| | | The following paper and the software described in it is now available online:
Siert Wieringa, Matti Niemenmaa and Keijo Heljanko, Tarmo: A Framework for Parallelized Bounded Model Checking, In Lubos Brim and Jaco van de Pol, editors, Proceedings of the 8th International Workshop on Parallel and Distributed Methods in verifiCation (PDMC09), volume 14 of Electronic Proceedings in Theoretical Computer Science (EPTCS), pages 62-76, 2009.
Our Tarmo framework is an approach to parallelizing BMC by parallel SAT solving of the sequence of incrementally encoded SAT instances that follow from a single BMC task. The satisfiability of an instance in such a sequence corresponds to the existence of a counterexample of a specific length. The available Tarmo software implements our generic shared clause database architecture which allows sharing clauses between SAT solver processes that are working on possibly different instances from one such sequence. |
| | | | |
| | |
| |
Call for Papers
Formal Methods and Verification Track
Design, Automation & Test in Europe
Dresden, Germany
March 8-12, 2010
The Design, Automation and Test in Europe conference and exhibition is the
premiere European event bringing together designers and design automation
users, researchers and vendors, as well as specialists in the hardware and
software design, test and manufacturing of electronic circuits and systems.
This five-day event consists of a conference with plenary keynotes, regular
papers, interactive presentations, panels and hot-topic sessions,
tutorials, master courses and workshops. DATE is also Europe's leading
commercial exhibition showing the state-of-the-art in design and test
tools, methodologies, IP and design services. Both the conference and the
exhibition, together with the many user group meetings, fringe meetings,
university booth and social events offer a wide variety of opportunities to
meet and exchange information.
The Formal Methods and Verification Track (D8) is devoted to the
presentation and discussion of state-of-the-art advances in a variety of
focus areas, including but not limited to:
* Formal verification and specification techniques including equivalence
checking, model checking, symbolic simulation, theorem-proving,
abstraction and refinement techniques, and real time verification
* Technologies supporting formal verification, including SMT, SAT, BDD,
ATPG, and related work
* Semi-formal verification techniques
* Applications and case studies, including formal verification of IPs,
SoCs, cores and real-time/embedded systems
* Verification in practice, namely the integration of verification into
the design flow
Jason Baumgartner (Chair) IBM Corporation, jason.r.baumgartner@gmail.com
Joao Marques-Silva (Co-Chair) University College Dublin, jpms@ucd.ie
Armin Biere Johannes Kepler University
Per Bjesse Synopsys Inc.
Roderick Bloem Graz University of Technology
Gianpiero Cabodi Politecnico di Torino
Alessandro Cimatti FBK-IRST
Daniel Kroening Oxford University
Wolfgang Kunz University of Kaiserslautern
Panagiotis Manolios Northeastern University
All manuscripts must be submitted electronically by September 6th, 2009,
following the instructions on the conference Web page:
www.date-conference.com
|
| | | | |
| | |
| | |
| |
