A System for Modelling and Proving Circuits
Abstract
We present the architecture of Formath: a system for modelling and proving circuits. Its core is a formal system, the P-calculus which allows to accurately describe structures and behaviours of circuits. In order to perform verifications, the P-calculus is implemented into proof assistants (LP and COQ). Different aspects of the system are depicted and illustrated by several examples.
References
[1]
{1} M. Allemand, S. Coupet-Grimal and J.L. Paillet FORMATH a system for modelling and proving circuits. RR 1995.106, LIM, Apr. 1995.
[2]
{2} G. Dowek, and all. The Coq Proof assistant User's Guide. TR 154, INRIA, CNRS, May 1993.
[3]
{3} S. Garland and J. Guttag. A guide to LP, the Larch Prover. RR 82, DEC SRC, Dec. 1991.
- A System for Modelling and Proving Circuits
Recommendations
Kripke modelling and verification of temporal specifications of a multiple UAV system
A verifiable multiple UAV system cooperatively monitoring a road network is presented in this paper. The focus is on formal modelling and verification which can guarantee correctness of concurrent reactive systems such as multi-UAV systems. Kripke ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
March 1996
585 pages
ISBN:0818674237
Copyright © Copyright (c) 1996 Institute of Electrical and Electronics Engineers, Inc. All rights reserved.
Sponsors
Publisher
IEEE Computer Society
United States
Publication History
Published: 11 March 1996
Check for updates
Qualifiers
- Article
Conference
EDTC96
Sponsor:
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 85Total Downloads
- Downloads (Last 12 months)40
- Downloads (Last 6 weeks)7
Reflects downloads up to 16 Nov 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in