Combining model checking and theorem proving to verify parallel processes
H Hungar - … Aided Verification: 5th International Conference, CAV' …, 1993 - Springer
To overcome the limitations of pure model checking, this verification technique is combined
with theorem proving. Large processes are split into components whose correctness wrt …
with theorem proving. Large processes are split into components whose correctness wrt …
Modeling a hardware synthesis methodology in Isabelle
D Basin, S Friedrich - Theorem Proving in Higher Order Logics: 9th …, 1996 - Springer
Formal Synthesis is a methodology developed at Kent for combining circuit design and
verification. We have reinterpreted this methodology in Isabelle's theory of higher-order logic …
verification. We have reinterpreted this methodology in Isabelle's theory of higher-order logic …
The need for a core method DIALOG—Linking formal proof to the design environment
EM Mayger, MD Francis, RL Harris, G Musgrave… - Microprocessing and …, 1991 - Elsevier
Recent techniques described in the literature for applying Formal Methods to Design
Verification are post design and require a deep knowledge of formal mathematics …
Verification are post design and require a deep knowledge of formal mathematics …
Representation engineering and category theory
RM Zimmer - Change of Representation and Inductive Bias, 1990 - Springer
The choice of representation can make an enormous difference to the ease with which a
problem can be solved. We would like to build a system that can help a programmer to …
problem can be solved. We would like to build a system that can help a programmer to …
Formal synthesis
MP Fourman, RA Hexsel - IV Higher Order Workshop, Banff 1990 …, 1991 - Springer
Most applications of formal proof to digital hardware have been aimed at proving the
correctness of existing designs. Here, we address the application of formal methods to the …
correctness of existing designs. Here, we address the application of formal methods to the …
Modeling a hardware synthesis methodology in Isabelle
D Basin, S Friedrich - Formal Methods in System Design, 1999 - Springer
Formal Synthesis is a methodology developed at the university of Kent for combining circuit
design and verification, where a circuit is constructed from a proof that it meets a given …
design and verification, where a circuit is constructed from a proof that it meets a given …
Formal derivation of a class of computers
LG Wang - 1995 - era.ed.ac.uk
The aim of this thesis is to investigate how to use logic-based specification, construction, and
proof methods to formally derive a class of computers. Differing from the traditional concepts …
proof methods to formally derive a class of computers. Differing from the traditional concepts …
The algebra of system design: A Petri net model of modular composition
R Zimmer, A MacDonald - 1993 IEEE International Symposium …, 1993 - ieeexplore.ieee.org
A mathematically-based CAD system is being designed. The system will have a predicate
logic theorem prover at its core, and will mirror every surface-level design step with an …
logic theorem prover at its core, and will mirror every surface-level design step with an …
CAD for verified hardware design via category theory
We are studying ways to incorporate hierarchic layered design style to a CAD system that
has a theorem prover at its core without destroying the mathematical foundation of the …
has a theorem prover at its core without destroying the mathematical foundation of the …
[PDF][PDF] Formal Methods for Modelling Wireless Sensor Networks
C Biró - 2019 - core.ac.uk
Formal Methods for Modelling Wireless Sensor Networks Page 1 Formal Methods for Modelling
Wireless Sensor Networks Theses of Ph.D. Dissertation Csaba Biró Eötvös Loránd University …
Wireless Sensor Networks Theses of Ph.D. Dissertation Csaba Biró Eötvös Loránd University …