loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
First ACM and IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE?03)
Combining ACL2 and a v-calculus Model-Checker to Verify System-Level Designs
Mont Saint-Michel, France
June 24-June 26
ISBN: 0-7695-1923-7
ASCII Text
x 
 
Magali Contensin, Laurence Pierre, "Combining ACL2 and a v-calculus Model-Checker to Verify System-Level Designs," Formal Methods and Models for Co-Design, ACM/IEEE International Conference on, pp. 75, First ACM and IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE?03), 2003.
 
 
BibTex
x
 
@article{ 10.1109/MEMCOD.2003.1210091,
author = {Magali Contensin and Laurence Pierre},
title = {Combining ACL2 and a v-calculus Model-Checker to Verify System-Level Designs},
journal ={Formal Methods and Models for Co-Design, ACM/IEEE International Conference on},
volume = {0},
year = {2003},
isbn = {0-7695-1923-7},
pages = {75},
doi = {http://doi.ieeecomputersociety.org/10.1109/MEMCOD.2003.1210091},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Formal Methods and Models for Co-Design, ACM/IEEE International Conference on
TI - Combining ACL2 and a v-calculus Model-Checker to Verify System-Level Designs
SN - 0-7695-1923-7
SP
EP
A1 - Magali Contensin,
A1 - Laurence Pierre,
PY - 2003
KW - null
VL - 0
JA - Formal Methods and Models for Co-Design, ACM/IEEE International Conference on
ER -
 
Magali Contensin, CMI/Universite
Laurence Pierre, I3S - Universite de Nice

The purpose of this paper is the formal verification of temporal properties of system-level descriptions that include both a control part, which corresponds to a finite set of symbolic states, and a data path with numeric variables. Keeping these variables under their numeric form, without assuming any encoding, induces an infinite state space.

We propose a combination of a model-checker for the modal ?-calculus with the theorem prover ACL2. Due to the induction mechanism of ACL2, this approach allows to consider the infinite state space without having to appeal to reduction techniques. Two simple but significant examples illustrate our results.

Citation:
Magali Contensin, Laurence Pierre, "Combining ACL2 and a v-calculus Model-Checker to Verify System-Level Designs," memocode, pp.75, First ACM and IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE?03), 2003
Usage of this product signifies your acceptance of the Terms of Use.