A Simple Calculus for Synthesizing Circuits (2008)
David Basin, Stefan Friedrich, Im Stadtwald
The task of developing correct hardware consists in designing an implementation of a circuit and after proving it to be correct with respect to its speci cation. In the discipline of hardware...
HOL-Z 2.0: A Proof Environment for Z-Specifications Extended Abstract (2008)
Achim D. Brucker, Stefan Friedrich, Frank Rittinger, Burkhart Wolff
The design of tools for formal specification languages (SL) can be roughly divided into two categories: special purpose design strives for implementing an SL and its method straight-forwardly in an...
Stefan Friedrich, Joachim Posegga, Harald Vogt, Deutsche Telekom Ag
Verification plays a central role in the security of Java bytecode: the Java bytecode verifier performs a static analysis to ensure that bytecode loaded over a network has certain security related...
Java Bytecode Verification by Model Checking (System Abstract) (2007)
David Basin, Stefan Friedrich, Joachim Posegga, Harald Vogt, Deutsche Telekom Ag
Verification plays a central role in the security of Java bytecode: the Java bytecode verifier performs a static analysis to ensure that bytecode loaded over a network has certain security related...
Veri ed Bytecode Model Checkers (2007)
David Basin, Stefan Friedrich, Marek Gawkowski
Abstract. We have used Isabelle/HOL to formalize and prove correct an approach to bytecode verication based on model checking that we have developed for the Java Virtual Machine. Our work builds on,...
HOL-Z 2.0: A Proof Environment for Z-Specifications Extended Abstract (2007)
Achim D. Brucker, Stefan Friedrich, Frank Rittinger, Burkhart Wolff
The design of tools for formal specification languages (SL) can be roughly divided into two categories: special purpose design strives for implementing an SL and its method straight-forwardly in an...
B2M: A Semantic Based Tool for BLIF Hardware Descriptions (2007)
David Basin, Stefan Friedrich, Sebastian Mödersheim
Abstract. BLIF is a hardware description language designed for the hierarchical description of sequential circuits. We give a denotational semantics for BLIF-MV, a popular dialect of BLIF, that...
Global Small Solutions of the Vlasov-Norstrom System (2004)
The Vlasov-Nordstrom system is a relativistic model for the description of a self-gravitating collisionless gas. In this paper we show, using a bootstrap argument, that classical small solutions of...
Bytecode Verification by Model Checking (2003)
David Basin, Stefan Friedrich, Marek Gawkowski
Java bytecode verification is traditionally performed using dataflow analysis. We investigate an alternative based on reducing bytecode verification to model checking. First, we analyze the...
Bytecode Verification by Model Checking (2003)
David Basin, Stefan Friedrich, Marek Gawkowski
Abstract. Java bytecode verification is traditionally performed using dataflow analysis. We investigate an alternative based on reducing bytecode verification to model checking. First, we analyze the...
Bytecode Model Checking: An Experimental Analysis (2002)
David Basin, Stefan Friedrich, Marek Gawkowski, Joachim Posegga
Abstract. Java bytecode verification is traditionally performed by a polynomial time dataflow algorithm. We investigate an alternative based on reducing bytecode verification to modelchecking....
Bytecode Model Checking: An Experimental Analysis (2002)
David Basin, Stefan Friedrich, Marek Gawkowski, Joachim Posegga
Abstract. Java bytecode verification is traditionally performed by a polynomial time dataflow algorithm. We investigate an alternative based on reducing bytecode verification to model checking....
Bytecode Model Checking: An Experimental Analysis (2002)
Stefan Friedrich, Marek Gawkowski, Joachim Posegga
Abstract. Java bytecode verication is traditionally performed by a polynomial time data ow algorithm. We investigate an alternative based on reducing bytecode verication to model checking. Despite an...
Verified bytecode model checkers (2002)
David Basin, Stefan Friedrich, Marek Gawkowski
Abstract. We have used Isabelle/HOL to formalize and prove correct an approach to bytecode verification based on model checking that we have developed for the Java Virtual Machine. Our work builds...
Proof Environment For, Achim D. Brucker, Stefan Friedrich, Frank Rittinger, Burkhart Wol
Achim D. Brucker, Stefan Friedrich, Frank Rittinger, and Burkhart Wol# Albert-Ludwigs-Universitat Freiburg {brucker,friedric,rittinge,wolff}@informatik.uni-freiburg.de 1
HOL-Z 2.0: A proof environment for Z-specifications (2002)
Achim D. Brucker, Stefan Friedrich, Frank Rittinger, Burkhart Wolff
The design of tools for formal specification languages (SL) can be roughly devided into two categories: special purpose design strives for implementing an SL and its method straight-forwardly in an...
Thesis (doctoral)--Technische Universität München, 2001.
We investigate the combination of the weak second-order monadic logic of one successor (WS1S) with higher-order logic (HOL). We show how these two logics can be combined, how theorem provers based on...
We investigate the combination of the weak second-order monadic logic of one successor (WS1S) with higher-order logic (HOL). We show how these two logics can be combined, how theorem provers based on...
Structural and Behavioral Modeling with Monadic Logics (1999)
Abdelwaheb Ayari David, David Basin, Stefan Friedrich
Logic offers the possibility of modeling and reasoning about hardware and software. But which logic? We propose monadic logics of strings and trees as good candidates for many kinds of discrete...
Structural and Behavioral Modeling with Monadic Logics (1999)
Abdelwaheb Ayari, David Basin, Stefan Friedrich
Logic offers the possibility of modeling and reasoning about hardware and software. But which logic? We propose monadic logics of strings and trees as good candidates for many kinds of discrete...
Dissertation (doctoral)--Albert-Ludwigs-Universität, Freiburg, 1998.
We investigate the combination of the weak second-order monadic logic of one successor (WS1S) with higher-order logic (HOL). We show how these two logics can be combined, how theorem provers based on...
Modeling a Hardware Synthesis Methodology in Isabelle (1996)
. Formal Synthesis is a methodology developed at Kent for combining circuit design and verification, where a circuit is constructed from a proof that it meets a given formal specification. We have...
Modeling a Hardware Synthesis Methodology in Isabelle (1996)
. 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 so that...
Mikrofiche-Ausg.: 3 Mikrofiches : 24x.
B2M: A Semantic Based Tool for BLIF Hardware Descriptions
David Basin, Stefan Friedrich, Sebastian Modersheim
. BLIF is a hardware description language designed for the hierarchical description of sequential circuits. We give a denotational semantics for BLIF-MV, a popular dialect of BLIF, that interprets...