| 9:00 - 10:30 |
Session 1
Session Chair: Miroslav N. Velev (Aries Design Automation, U.S.A.) |
| 9:00 - 10:30 |
Invited Talk: Treating Constraints as Components: An Experiment in User Control
Carl-Johan H. Seger (Intel, U.S.A.)
|
| 10:30 - 10:45 |
Break |
| 10:45 - 12:15 |
Session 2
Session Chair: Sumit K. Jha (University of Central Florida, U.S.A.) |
| 10:45 - 11:15 |
Towards Proving TLM Properties with Local Variables
Hoang M. Le, Daniel Große, and Rolf Drechsler (University of Bremen, Germany)
|
| 11:15 - 11:45 |
Preprocessing Polynomials for Arithmetic Reasoning within the SMT-Solver STABLE
Alexander Dreyer (Fraunhofer Institute for Industrial Mathematics, Germany), Oliver Marx, Evgeny Pavlenko, Markus Wedler, Dominik Stoffel, Wolfgang Kunz, and Gert-Martin Greuel (University of Kaiserslautern, Germany)
|
| 11:45 - 12:15 |
On Formal Verification of Pipelined Processors with Arrays of Reconfigurable Functional Units
Miroslav N. Velev, and Ping Gao (Aries Design Automation, U.S.A.)
|
| 12:15 - 13:30 |
Lunch (Provided) |
| 13:30 - 15:30 |
Session 3
Session Chair: Daniel Große (University of Bremen, Germany) |
| 13:30 - 14:30 |
Invited Talk: Using Constraint Solvers in Interactive and Automated Theorem Proving
Natarajan Shankar (SRI, U.S.A.)
|
14:30 - 15:00 |
Discovering Rare Behaviors of Stochastic Models Using Decision Procedures
Arup K. Ghosh, Emily Sassano, Sumit K. Jha (University of Central Florida, U.S.A.), Christopher J. Langmead (Carnegie Mellon University, U.S.A.), and Susmit Jha (University of California at Berkeley, U.S.A.)
|
15:00 - 15:30 |
Formally Verifying Expert Conjectures on Extreme Scale Data
Sumit K. Jha, Raj G. Dutta, and Emily Sassano (University of Central Florida, U.S.A.)
|
| 15:30 - 16:00 |
Break |
| 16:00 - 17:30 |
Session 4
Session Chair: Evgeny Pavlenko (University of Kaiserslautern, Germany) |
| 16:00 - 16:30 |
Post-Silicon Debugging of Many-Core Systems by Identifying Execution Paths Through Constraint Refinement
Amir M. Gharehbaghi, and Masahiro Fujita (University of Tokyo, Japan)
|
| 16:30 - 17:00 |
Bounded Model Checking and Feature Omission Diversity
Amin Alipour, and Alex D. Groce (Oregon State University, U.S.A.)
|
| 17:00 - 17:30 |
Propelling SAT-Based Debugging Using Reverse Domination
Bao Le, Hratch Mangassarian, Brian Keng, and Andreas Veneris (University of Toronto, Canada)
|
Formal verification is of crucial significance in the development of
hardware and software systems. In the last few years, tremendous
progress was made in both the speed and capacity of constraint
technology. Most notably, SAT solvers have become orders of magnitude
faster and capable of handling problems that are orders of magnitude
bigger, thus enabling the formal verification of more complex computer
systems. As a result, the formal verification of hardware and software
has become a promising area for research and industrial applications.
The main goals of the Constraints in Formal Verification
workshop are to bring together researchers from the CSP/SAT and the
formal verification communities, to describe new applications of
constraint technology to formal verification, to disseminate new
challenging problem instances, and to propose new dedicated algorithms
for hard formal verification problems.
This workshop will be
of interest to researchers from both academia and industry, working on
constraints or on formal verification and interested in the application
of constraints to formal verification.
Scope
The scope of the workshop includes topics related to the application
of constraint technology to formal verification, namely:
-
application of constraint solvers to hardware verification;
-
application of constraint solvers to software verification;
-
dedicated solvers for formal verification problems;
-
challenging formal verification problems.
Location
The workshop will take place in the DoubleTree Hotel in San Jose, California, on November 10, 2011, right after ICCAD'11. It will be structured
to allow ample time for discussion and demonstration of new tools and new problem instances.
Submissions
Submissions should be in the IEEE style
and in one of the following types:
- a regular paper of up to 6 pages;
- a short paper of up to 4 pages, describing an industrial experience.
Papers should be e-mailed in pdf format to the workshop chair:
mvelev@gmail.com
Important Dates
The important dates for the workshop are as follows:
| Abstract submission deadline | September 25 |
| EXTENDED Paper submission deadline | October 3 |
| Notification of acceptance | October 10 |
| Camera-ready version deadline | October 25 |
| Workshop date | November 10 |
Invited Speakers
Carl-Johan H. Seger,
Intel, U.S.A.
Talk title: Treating Constraints as Components: An Experiment in User Control
Natarajan Shankar,
SRI, U.S.A.
Talk title: Using Constraint Solvers in Interactive and Automated Theorem Proving
Workshop Chair
Miroslav Velev, Aries Design Automation, U.S.A.
Email: mvelev@gmail.com
Program Committee
Maciej Ciesielski, University of Massachusetts, U.S.A.
Masahiro Fujita, University of Tokyo, Japan
Alex D. Groce, Oregon State University, U.S.A.
Daniel Grosse, University of Bremen, Germany
Michael Hsiao, Virginia Tech, U.S.A.
Sumit Jha, University of Central Florida, U.S.A.
Robert Jones, Intel, U.S.A.
Peter-Michael Seidel, AMD, U.S.A.
Andreas Veneris, University of Toronto, Canada
Markus Wedler, University of Kaiserslautern, Germany
|