 |
12 elements available | |
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) |
| |  | |  |
| | |
| |
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
|
| | | | |
| | |
|  | |  | | | | | Date: | 11-May-2009 | | Title: | HLDVT 2009: Call for Papers
| | Hits: | 555 | | Contributed by: | Anonymous | | Keywords: | BDD, Random 3SAT, Verification, EDA, Benchmark, SAT application, Equivalency Reasoning, SAT tools, call for papers, SAT-Based, SAT/CP, Hybrid solver, null, null, null, null, null |
| | | |  |  | |
| | | Call for Papers
***************************************************************
HLDVT 2009
IEEE International High-Level Design, Validation and Test Workshop
http://www.hldvt.com/09/
Grand Hyatt, San Francisco, California, November 4-6, 2009
***************************************************************
Please visit http://www.hldvt.com/09/HLDVT09_cfp.pdf |
| | | | |
| | |
| |
Applied Formal Verification Track
EUROCAST'09
Las Palmas, Canary Islands, Spain
IMPORTANT DATES
February 15-20, 2009
Ext. Abstracts: 31. Oktober, 2008 (2 pages LNCS style)
Conference: 15.-20. February, 2009
Full Papers: 30. April, 2009 (prob. again in LNCS)
http://www.iuctc.ulpgc.es/spain/eurocast2009/index.html
TOPICS
In the last decade the topic of formal verification has left
the ivory tower of academic research. In hardware design many
industrial projects rely in one way or the other on formal
verification tools. The same trend can be seen in software.
The main driving force behind this development is on one hand
the increasing complexity of todays design, which can not
be handled by traditional testing techniques alone, and on
the other hand by the increasing dependability of our daily
lives on computer systems. However, also the core engines,
such as SAT solvers are becoming much more powerful.
In this workshop we want to bring to together researchers in
applied formal verification. We focus on formal verification
engines. The topics include, but are not limited to the
following
Satisfiability (SAT)
Satisfiability Modulo Theories (SMT)
Quantified Boolean Formulas (QBF)
Constraint Programming (CP)
Equivalence Checking (EC)
Model Checking (MC)
Theorem Proving (TP)
Beside papers on verification engines we also welcome case
studies and papers on the border line of verification, including
synthesis, compilation and modelling. Our main goal is to
improve practicability and scalability of formal methods.
SUBMISSION
An extended two pages abstract, including references in English
with indication of the workshop of the intended contribution,
e.g. 'Applied Formal Verification' must be sent (via webpage or
by e-mail) before October, 31, 2008 to the Organizing Commitee
Chairman: aquesada@dis.ulpgc.es.
|
| | | | |
| | |
| | | | | | | | Date: | 09-Jul-2008 | | Title: | DATE09 Call for Papers -- Formal Methods and Verification Track
| | Hits: | 886 | | Contributed by: | | |
Volume 5 Contents
Special Volume on Application of Constraints to Formal Verification
Editor: Miroslav Velev
Miroslav N. Velev. Editor's Introduction to the Special Volume on Application of Constraints to Formal Verification.
Articles
Sean Safarpour, Andreas Veneris, and Rolf Drechsler. Improved SAT-based Reachability Analysis with
Observability Don't Cares. Volume 5 (2008), pages 1-25.
* Keywords: SAT solver, reachability analysis, model checking, observability don't cares.
Javier Esparza, Stefan Kiefer, and Stefan Schwoon. Abstraction Refinement with Craig Interpolation
and Symbolic Pushdown Systems. Volume 5 (2008), pages 27-56.
* Keywords: model-checking, abstraction refinement, Craig interpolation, BDDs, pushdown systems.
Masahiro Fujita, Kenshu Seto, and Thanyapat Sakunkonchak. Dependence Graph Based Verification and
Synthesis of Hardware/Software Co-Designs with SAT Related Formulation. Volume 5 (2008), pages 57-82.
* Keywords: SAT-solver, lookahead, equivalence reasoning, local learning.
Viviana Bruno, Luz Garcia, Sergio Nocco, and Stefano Quer. Stressing Symbolic Scheduling Techniques
within Aircraft Maintenance Optimization. Volume 5 (2008), pages 83-110.
* Keywords: Boolean satisfiability, SAT-solvers, timed automata, Petri nets, scheduling, planning.
Sergio Nocco and Stefano Quer. A Probabilistic and Approximated Approach to Circuit-Based Formal
Verification. Volume 5 (2008), pages 111-132.
* Keywords: and-inverter graph, Boolean satisfiability, SAT-solvers, model checking, density, controllability.
Marco Benedetti and Hratch Mangassarian. QBF-Based Formal Verification: Experience and Perspectives.
Volume 5 (2008), pages 133-191.
* Keywords: quantied Boolean formulas, formal verification, empirical evaluation.
Michael Codish, Vitaly Lagoon, and Peter J. Stuckey. Solving Partial Order Constraints for LPO
Termination. Volume 5 (2008), pages 193-215.
* Keywords: Boolean satisfiability, lexicographic path orders, proving termination, term rewrite systems.
Research notes
Eugene Goldberg. A Resolution Based SAT-solver Operating on Complete Assignments. Volume 5 (2008),
research note, pages 217-242.
* Keywords: SAT-solver, resolution, decision-making, local search, complete assignment.
Lei Fang and Michael S. Hsiao. Boosting SAT Solver Performance via a New Hybrid Approach. Volume 5
(2008), research note, pages 243-261.
* Keywords: satisfiability, DPLL, WalkSAT, hybrid.
|
| | | | |
| | |
| | | | | | | | Date: | 16-Jan-2008 | | Title: | E.Goldberg. On bridging simulation and formal verification, VMCAI-2008, San Francisco, USA, LNCS 4905, pp.127-141
| | Hits: | 785 | | Contributed by: | | | | | | | | | Date: | 07-Jan-2008 | | Title: | Practical SAT: A tutorial on applied satisfiability solving, Niklas Een, FMCAD, November 11, 2007
| | Hits: | 1304 | | Contributed by: | Daniel Le Berre | | Keywords: | DPLL, Data structure, Verification, Structure of problems, EDA, SAT application, Instance simplification, Learning, SAT tools, branching heuristics, Dynamic restarts, variable ordering heuristic, General Interest, SAT-Based, SAT-solver, null, null, null |
| | | | | | |
| | From the presentation web page:
The presentation consists of five programs (4 binaries, 1 source code):
* PracticalSAT: Views the slides. Will provide documentation upon run.
* MiniSat_demo: Shows inner workings of MiniSat.
* MiniSat_viz: Visualizes certain key parameters of the SAT run.
* SatELite_demo: Demonstrates CNF preprocessing.
* OptSynth: Source code for a program solving the synthesis problem
discussed in the slides using MiniSat.
A zip file containing all the executables for Linux is available here.
The zip file expands into a directory named PracticalSAT. The directory also
contains additional README files with more information on how to use the three latter programs.
Updated: changed link to minisat page with linux, cygwin and windows binaries.
|
| | | | |
| | |
| | | | | | | | Date: | 15-Nov-2007 | | Title: | Post-Doctoral Position
| | Hits: | 1235 | | Contributed by: | | |
Avionic platforms require more and more software. Such software have
to satisfy safety, security and disponibilty requirements. The
architecture of the related applications raise as well software
development problems as well as hardware configuration problems.
In this study, we are interested in software environments for the
development of such applications and also in synthesis and
verification tools~(linear algebra, SAT based, ...) for the
development assistance.
We are interested in model based development approach. After a first
year where we have studied alternative data models, now, we have to
study how such models will be mapped to verification languages using a
transformation based approach. Moreover, the experimentation of
verification tools will have to be completed.
Related domains:
Verification and synthesis tools, real time, model based development,
Java, Eclipse.
Gross annual salary: 24000 Euros
locaion: IRIT
Université Paul Sabatier
F-31062 Toulouse
France
contact: filali@irit.fr
citizenship: french or UE citizenship is required.
|
| | | | |
| | |
| | |
|
|
|
|
|
|
|
|
|
| |
