DocumentCode
500811
Title
Constraints in one-to-many concretization for abstraction refinement
Author
Nanshi, Kuntal ; Somenzi, Fabio
Author_Institution
Univ. of Colorado at Boulder, Boulder, CO, USA
fYear
2009
fDate
26-31 July 2009
Firstpage
569
Lastpage
574
Abstract
In one-to-many concretization for model checking based on abstraction refinement, constraints on input vectors that are pseudorandomly generated are often essential to the success of the procedure. These constraints have to do with both primary inputs and invisible state variables. We discuss algorithms that address both types and we show their effectiveness through experiments.
Keywords
formal verification; abstraction refinement; invisible state variable; model checking; one-to-many concretization; pseudorandom generation; Algorithm design and analysis; Boolean functions; Computer bugs; Concrete; Contracts; Data structures; Discrete event simulation; Event detection; Logic design; Permission; abstraction refinement; model checking; simulation;
fLanguage
English
Publisher
ieee
Conference_Titel
Design Automation Conference, 2009. DAC '09. 46th ACM/IEEE
Conference_Location
San Francisco, CA
ISSN
0738-100X
Print_ISBN
978-1-6055-8497-3
Type
conf
Filename
5227066
Link To Document