salle A. Turing CE4
19 mars 2013 - 11h00
Integrating Induction and Deduction for Verification and Synthesis
par Sanjit Seshia de University of California, Berkeley
Abstract: Even with impressive advances in automated formal methods, certain
problems in system verification and synthesis remain challenging.
Examples include the verification of quantitative properties of software
involving constraints on timing and energy consumption, and the
automatic synthesis of systems from specifications. The challenges
mainly arise from three sources: environment modeling, incompleteness
in specifications, and the complexity of underlying decision problems.
In this talk, I will present sciduction, a methodology to tackle these
challenges. Sciduction combines inductive inference (learning from examples),
deductive reasoning (such as SAT/SMT solving), and structure hypotheses.
We have demonstrated several applications of sciduction including timing
analysis of embedded software, synthesis of loop-free programs, synthesis
from temporal logic (LTL), term-level verification of hardware (RTL) designs,
and switching logic synthesis of hybrid systems. This talk will present some
core theory, a couple of illustrative applications (switching logic
synthesis and synthesis from LTL), and directions for future work.
Brief Biography available here:
http://www.eecs.berkeley.edu/~sseshia/bio.html
