Secure Neighborhood Discovery: A Fundamental Element for Mobile Ad Hoc Networking (2009)
Panos Papadimitratos, Marcin Poturalski, Patrick Schaller, Pascal Lafourcade, David Basin, Srdjan Čapkun, ...
Abstract—Pervasive computing systems will likely be deployed in the near future, with the proliferation of wireless devices and the emergence of ad hoc networking as key enablers. Coping with...
Semester Thesis A Software-based TPM Emulator for Linux Supervisors: (2008)
Paul E. Sevinç, Prof Dr, David Basin, Mario Strasser
The Trusted Computing Group (TCG) has produced several specifications for trusted computing such as for a security chip, called Trusted Platform Module (TPM), and for related software interfaces (TCG...
Computer Supported Modeling and Reasoning (2008)
Metatheory Ii Rules, David Basin
Last lecture: simple types for representing syntax. For representing rules and proofs, need type “proof of a”. Such a type is called dependent. System LF.
Abstract Automated Analysis of Security-Design Models (2008)
We have previously proposed SecureUML, an expressive UML-based language for constructing security-design models, which are models that combine design specifications for distributed systems with...
Here there is no meta/object distinction. Everything is defined within HOL. Reasoning is classical. • Still modeling of problems/domains is important (now within HOL) So is deriving relevant...
A Monad-based Modeling and Verification Toolbox with Application to Security Protocols ⋆ (2008)
Christoph Sprenger, David Basin
Abstract. We present an advanced modeling and verification toolbox for functional programs with state and exceptions. The toolbox integrates an extensible, monad-based, component model, a monad-based...
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...
David Basin, Jürgen Doser, Torsten Lodderstedt
Abstract We present a new approach to building secure systems. In our approach, which we call Model Driven Security, designers specify system models along with their security requirements and use...
Doktors der Naturwissenschaften (Dr. rer. nat.) genehmigten Dissertation. (2008)
Konrad Slind, Steger Pr"ufer Dissertation, ...
Abstract This thesis addresses two basic problems with the current crop of mechanized proof systems. The first problem is largely technical: the act of soundly introducing a recursive definition is...
• Formalizing Class Diagrams (2008)
David Basin, Achim D. Brucker, Jan-georg Smaus, Burkhart Wolff, Achim D. Brucker
• Embedding OCL into Isabelle/HOL • Conclusion
Deconstructing Alice, Carlos Caleiro, Luca Viganò, David Basin
Alice&Bob–notation is a simple notation for describing security protocols as sequences of message exchanges. We show that, despite the fact that Alice&Bob–notation does not include...
Information Security Group (2008)
David Basin, Jürgen Doser, Eth Zürich
Security-design models are models that combine design specifications for distributed systems with specifications of their security policies. We have previously proposed an expressive UML-based...
BAP: Broadcast Authentication Using Cryptographic Puzzles (2008)
Patrick Schaller, Srdjan Čapkun, David Basin
We present two broadcast authentication protocols based on delayed key disclosure. Our protocols rely on symmetric-key cryptographic primitives and use cryptographic puzzles to provide efficient...
Proof Environments for Formal Specification Languages (2008)
David Basin, Achim D. Brucker, Jan-georg Smaus, Burkhart Wolff, Winter Term, Achim D. Brucker
Isabelle is not alone there are many successful theorem provers, e.g.: • Coq:
Technical Report No. 526 Timing-Sensitive Information Flow Analysis for Synchronous Systems (2008)
Abstract. Timing side channels are a serious threat to the security of cryptographic algorithms. This paper presents a novel method for the timing-sensitive analysis of information flow in...
Specifying and Analyzing Security Automata using CSP-OZ ∗ (2008)
Security automata are a variant of Büchi automata used to specify security policies that can be enforced by monitoring system execution. In this paper, we propose using CSP-OZ, a specification...
David Basin, Hironobu Kuruma, Kunihiko Miyazaki, Kazuo Takaragi, Burkhart Wolff
Abstract. We report on a case study in applying different formal methods to model and verify an architecture for administrating digital signatures. The architecture comprises several concurrently...
A Proof of Concept Implementation of SSL/TLS Session-Aware User Authentication (TLS-SA) (2008)
Abstract Most SSL/TLS-based e-commerce applications employ conventional mechanisms for user authentication. These mechanisms—if decoupled from SSL/TLS session establishment—are vulnerable to...
Midpoints versus Endpoints From Protocols to Firewalls ⋆ (2008)
Abstract. Today’s protocol specifications only define the behaviour of principals representing communication endpoints. But in addition to endpoints, networks contain midpoints, which are machines...
SSL/TLS Session-Aware User Authentication Revisited,” submitted for publication (2008)
Ralf Hauser, David Basin, Privasphere Ag
Abstract. Man-in-the-middle (MITM) attacks pose a serious threat to SSL/TLS-based e-commerce applications, and there are only a few technologies available to mitigate the risks. In [OHB05], we...
Submitted to Communications of the ACM. Model Driven Security (2008)
David Basin, Eth Zürich, Martin Buchheit, Interactive Objects, Software Gmbh, Jürgen Doser, ...
We present Model Driven Security, a new approach to building secure systems. In Model Driven Security, designers specify high-level system models along with their security properties and use tools to...
Formalizing and Analyzing Sender Invariance ⋆ (2008)
Paul Hankes Drielsma, Sebastian Mödersheim, Luca Viganò, David Basin
Abstract. In many network applications and services, agents that share no secure channel in advance may still wish to communicate securely with each other. In such settings, one often settles for...
A Proof of concept Implementation of SSL/TLS Session-Aware User Authentication (2008)
Ralf Hauser, David Basin, Aldo Rodenhaeuser
Abstract. Man-in-the-middle (MITM) attacks pose a serious threat to SSL/TLS-based e-commerce applications, such as Internet banking. SSL/TLS session-aware user authentication can be used to mitigate...
Labeled tableaux for distributed temporal logic ⋆ (2008)
David Basin, Carlos Caleiro, Jaime Ramos, Luca Viganò
Abstract. DTL is a distributed temporal logic for reasoning about temporal properties of distributed systems from the local point of view of the system’s agents, which are assumed to execute...
Deconstructing Alice, Carlos Caleiro, Luca Viganò, David Basin
We show that, despite the fact that Alice&Bob–notation does not include explicit control flow constructs, it is possible to make some of these aspects explicit and thus produce formal protocol...
Runtime Monitoring of Metric First-order Temporal Properties (2008)
Basin, David, Klaedtke, Felix, Müller, Samuel, Pfitzmann, Birgit
We introduce a novel approach to the runtime monitoring of complex system properties. In particular, we present an online algorithm for a safety fragment of metric first-order temporal logic that is...
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...
Categories and Subject Descriptors (2007)
David Basin, Jürgen Doser, Torsten Lodderstedt
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial...
Decision procedures for inductive Boolean (2007)
Abdelwaheb Ayari, David Basin, Felix Klaedtke, Communicated W. Thomas
functions based on alternating automata
Rafael Accorsi, David Basin, Luca Vigan
an awareness-based semantics for security protocol analysis
Qubos: Deciding Quantied Boolean Logic using Propositional Satisability Solvers (2007)
www.informatik.uni-freiburg.de/fayarijbasing
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,...
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...
A Formal Data-Model of the CORBA Security Service (2007)
David Basin, Frank Rittinger, Luca Vigan
We use the formal language Z to specify and analyze the security service of CORBA. In doing so, we tackle the problem of how one can apply lightweight formal methods to improve the precision and aid...
A Formal Analysis of the CORBA Security (2007)
Abstract. We give a formal specication and analysis of the security service of CORBA, the Common Object Request Broker Architecture speci ed by the Object Management Group, OMG. In doing so, we...
David Basin, Jürgen Doser, Torsten Lodderstedt
We present a new approach to building secure systems. In our approach, which we call model driven security, designers specify system models along with their security requirements and use tools to...
Towards a Metalogic for Security Protocol Analysis (Extended Abstract) (2007)
Carlos Caleiro, Luca Vigano, David Basin
Carlos Caleiro Luca Vigano David Basin CLC, Department of Mathematics, IST, Lisbon, Portugal cs.math.ist.utl.pt/ccal.html Department of Computer Science, ETH Zurich, Switzerland www.infsec.ethz.ch/ #...
A metamodel-based approach for analyzing security-design models (2007)
David Basin, Manuel Clavel, Jürgen Doser, Marina Egea
Abstract We have previously proposed an expressive UML-based language for constructing and transforming security-design models, which are models that combine design specifications for distributed...
SSL/TLS Session-Aware User Authentication—Or How to Effectively Thwart the Man-in-the-Middle (2006)
Ralf Hauser, David Basin, Privasphere Ag
Abstract. Man-in-the-middle attacks pose a serious threat to SSL/TLSbased electronic commerce applications, such as Internet banking. In this paper, we argue that most deployed user authentication...
Model Driven Security: from UML Models to Access Control Infrastructures (2006)
David Basin, Jürgen Doser, Torsten Lodderstedt
We present a new approach to building secure systems. In our approach, which we call Model Driven Security, designers specify system models along with their security requirements and use tools to...
Distributed Usage Control (2006)
Er Pretschner, Manuel Hilty, David Basin
Computer systems play an increasingly prominent role in our daily lives. Interacting with these systems often involves disclosing personal data, i.e., data that can be traced back to particular...
Cryptographically Sound Theorem Proving (2006)
Christoph Sprenger, Michael Backes, David Basin, Birgit Pfitzmann, Michael Waidner
We describe a faithful embedding of the Dolev-Yao model of Backes, Pfitzmann, and Waidner (CCS 2003) in the theorem prover Isabelle/HOL. This model is cryptographically sound in the strong sense of...
The AVISPA Tool for the automated validation of internet security protocols and applications (2005)
Armando, Alessandro, Basin, David, Boichut, Yohan, Chevalier, Yannick, Compagna, Luca, Cuellar, Jorge, ...
AVISPA is a push-button tool for the automated validation of Internet security-sensitive protocols and applications. It provides a modular and expressive formal language for specifying protocols and...
Algebraic intruder deductions (2005)
David Basin, Sebastian Mödersheim, Luca Viganò
Abstract. Many security protocols fundamentally depend on the algebraic properties of cryptographic operators. It is however difficult to handle these properties when formally analyzing protocols,...
• Formalizing Class Diagrams (2005)
David Basin, Achim D. Brucker, Jan-georg Smaus, Burkhart Wolff, Achim D. Brucker
David Basin, Achim D. Brucker, Jan-georg Smaus, Burkhart Wolff, Burkhart Wolff, Well-founded Orders
◦ Z and Data-Refinement,
David Basin, Achim D. Brucker, Jan-georg Smaus, Burkhart Wolff, Burkhart Wolff, Scons X Y
We are still looking at how the different parts of mathematics are encoded in the Isabelle/HOL library.
Higher-Order Logic (HOL) is: (2005)
David Basin, Achim D. Brucker, Jan-georg Smaus, Burkhart Wolff, David Basin
Higher-Order Logic (HOL) is: • an expressive foundation for mathematics: analysis, algebra,... computer science: program correctness, hardware verification,...
Manuel Hilty, David Basin, Er Pretschner
Abstract. Access control is concerned with granting access to sensitive data based on conditions that relate to the past or present, so-called provisions. Expressing requirements from the domain of...
Algebraic intruder deductions (2005)
David Basin, Sebastian Mödersheim, Luca Viganò
Abstract. Many security protocols fundamentally depend on the algebraic properties of cryptographic operators. It is however difficult to handle these properties when formally analyzing protocols,...
Verification of a signature architecture with HOL-Z (2005)
David Basin, Hironobu Kuruma, Kazuo Takaragi, Burkhart Wolff
Abstract. We report on a case study in using HOL-Z, an embedding of Z in higher-order logic, to specify and verify a security architecture for administering digital signatures. We have used HOL-Z to...
Relating Strand Spaces and Distributed Temporal Logic for Security Protocol Analysis (2005)
Caleiro, Carlos, Viganò, Luca, Basin, David
In previous work, we introduced a version of distributed temporal logic that is well-suited both for verifying security protocols and as a metalogic for reasoning about, and relating, different...
Metareasoning about Security Protocols using Distributed Temporal Logic (2004)
Carlos Caleiro, Luca Viganò, David Basin
We introduce a version of distributed temporal logic for rigorously formalizing and proving metalevel properties of different protocol models, and establishing relationships between models. The...
Metareasoning about Security Protocols using Distributed Temporal Logic (2004)
Carlos Caleiro, Luca Vigano, David Basin
We introduce a version of distributed temporal logic that provides a new basis to rigorously investigate general metalevel properties of di#erent protocol models, by establishing modeling and...
Synthesis of programs in computational logic (2004)
David Basin, Yves Deville, Pierre Flener, Andreas Hamfelt, Jørgen Fischer Nilsson, Mathematical Modelling
Abstract. Since the early days of programming and automated reasoning, researchers have developed methods for systematically constructing programs from their specifications. Especially the last...
Metareasoning about Security Protocols using Distributed Temporal Logic (2004)
Carlos Caleiro, Luca Viganò, David Basin
We introduce a version of distributed temporal logic for rigorously formalizing and proving metalevel properties of different protocol models, and establishing relationships between models. The...
Technical Report No. 450 OFMC: A Symbolic Model-Checker for Security Protocols ∗ (2004)
David Basin, Sebastian Mödersheim, Luca Viganò
We present the on-the-fly model-checker OFMC, a tool that combines two ideas for analyzing security protocols based on lazy, demand-driven search. The first is the use of lazy datatypes as a simple...
Modular Proof Systems for Partial Functions with Weak Equality (2004)
Ganzinger, Harald, Sofronie-Stokkermans, Viorica, Waldmann, Uwe, Basin, David, Rusinowitch, Michael
The paper presents a modular superposition calculus for the combination of first-order theories involving both total and partial functions. Modularity means that inferences are pure, only involving...
A Resolution Decision Procedure for the Guarded Fragment with Transitive Guards (2004)
Kazakov, Yevgeny, De Nivelle, Hans, Basin, David, Rusinowitch, Michael
We show how well-known refinements of ordered resolution, in particular redundancy elimination and ordering constraints in combination with a selection function, can be used to obtain a decision...
Bernd Krieg-brückner, Arne Lindow, Christoph Lüth, Achim Mahnke, George Russell, ...
MMiSS Multi-Media Instruction in Safe and Secure Systems 4
Theorem Proving in Higher Order Logics (2003)
David Basin, Burkhart Wolff (eds.), Eth Zentrum, Burkhart Wolff
Algebra in Type Theory with Dependent Records . . . 13 Xin Yu, Aleksey Nogin, Alexei Kopylov and Jason Hickey Implementing and Automating Basic Number Theory in MetaPRL Proof Assistant . . . . . . ....
Technical Report No. 404 An On-The-Fly Model-Checker for Security Protocol Analysis (2003)
David Basin, Sebastian Mödersheim, Luca Viganò
We introduce the on-the-fly model-checker OFMC, a tool that combines two ideas for analyzing security protocols based on lazy, demand-driven search. The first is the use of lazy data-types as a...
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...
David Basin, Jürgen Doser, Torsten Lodderstedt
We present a new approach to building secure systems. In our approach, which we call model driven security, designers specify system models along with their security requirements and use tools to...
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....
SecureUML: A UML-Based Modeling Language for Model-Driven Security (2002)
Torsten Lodderstedt, David Basin, Jürgen Doser
Abstract. We present a modeling language for the model-driven development of secure, distributed systems based on the Unified Modeling Language (UML). Our approach is based on role-based access...
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....
QUBOS: Deciding quantified Boolean logic using propositional satisfiability solvers (2002)
www.informatik.uni-freiburg.de/∼{ayari|basin}
Modal Specifications of Trace-Based Security Properties (2002)
Rafael Accorsi, David Basin, Luca Vigan
We introduce a multi-modal logic that combines complementary features of authentication logics and trace-based approaches. Our logic contains two kinds of modalities: implicit belief, which...
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...
A formal analysis of the CORBA security service (2002)
We give a formal specication of the security service of CORBA, the Common Object Request Broker Architecture speci ed by the Object Management Group, OMG. In doing so, we tackle the problem of how...
SecureUML: A UML-Based Modeling Language for (2002)
Torsten Lodderstedt, David Basin, Jrgen Doser
We present a modeling language for the model-driven development of secure, distributed systems based on the Unified Modeling Language (UML).
Modal Specifications of Trace-Based Security Properties (2002)
Rafael Accorsi, David Basin, Luca Viganò
We introduce a multi-modal logic that combines complementary features of authentication logics and trace-based approaches. Our logic contains two kinds of modalities: implicit belief, which...
A higher-order interpretation of deductive tableau (2001)
The Deductive Tableau of Manna and Waldinger is a formal system with an associated methodology for synthesizing functional programs by existence proofs in classical rst-order theories. We reinterpret...
Decision procedures for inductive boolean functions based on alternating automata (2000)
Abdelwaheb Ayari, David Basin, Felix Klaedtke
We show how alternating automata provide decision procedures for the equality of inductively dened Boolean functions and present applications to reasoning about parameterized families of circuits. We...
Decision procedures for inductive boolean functions based on alternating automata (2000)
Abdelwaheb Ayari, David Basin, Felix Klaedtke
We show how alternating automata provide decision procedures for the equality of inductively dened Boolean functions and present applications to reasoning about parameterized families of circuits. We...
Decision procedures for inductive boolean functions based on alternating automata (2000)
Abdelwaheb Ayari, David Basin, Felix Klaedtke
We show how alternating automata provide decision procedures for the equality of inductively dened Boolean functions and present applications to reasoning about parameterized families of circuits. We...
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...
Decision Procedures for Inductive Boolean Functions based on Alternating Automata (2000)
Abdelwaheb Ayari David, David Basin, Felix Klaedtke
. We show how alternating automata provide decision procedures for the equivalence of inductively dened Boolean functions that are useful for reasoning about parameterized families of circuits. We...
David Basin, Marcello D'Agostino, Dov M. Gabbay, Seán Matthews, Luca Viganò (eds.), An Matthews
In this paper, we propose new labelled proof systems to analyse the intuitionistic provability in classical and linear logics. An important point is to understand how search in a non-classical logic...
Rewriting Logic as a Metalogical Framework (2000)
David Basin, Manuel Clavel, José Meseguer
A metalogical framework is a logic with an associated methodology that is used to represent other logics and to reason about their metalogical properties. We propose that logical frameworks can be...
Combining Knowledge and Search to Solve Single-suit Bridge (2000)
Ian Frank, David Basin, Alan Bundy
In problem solving, it is often important not only to nd a solution but also to be able to explain it. We use the game of Bridge to illustrate how tactics, which formalise domain-specic expertise,...
Bounded Model Construction for Monadic Second-Order Logics (2000)
The monadic logics M2L-Str and WS1S have been successfully used for verification, although they are nonelementary decidable. Motivated by ideas from bounded model checking, we investigate procedures...
Bounded Model Construction for Monadic Second-Order Logics (2000)
Abdelwaheb Ayari And, Abdelwaheb Ayari, David Basin
. The monadic logics M2L-Str and WS1S have been successfully used for verication, although they are nonelementary decidable. Motivated by ideas from bounded model checking, we investigate procedures...
Maude versus Haskell: an Experimental Comparison in Security Protocol Analysis (2000)
We compare two executable languages: the rewriting logic based specification language Maude and the higher-order, lazy, functional programming language Haskell. We compare these languages...
Structuring Metatheory on Inductive Definitions (2000)
We examine a problem for machine supported metatheory. There are statements true about a theory that are true of some (but only some) extensions; however standard theory-structuring facilities do not...
Solving Single-suit Bridge Play: Winning and Knowing Why (2000)
Ian Frank, David Basin, Alan Bundy
In problem solving, it is often important not only to nd a solution but also to be able to explain it. We use the game of Bridge to illustrate how tactics, which formalise domain specic expertise,...
Rewriting Logic as a Metalogical Framework (2000)
David Basin, Manuel Clavel, José Meseguer
A metalogical framework is a logic with an associated methodology that is used to represent other logics and to reason about their metalogical properties. We propose that logical frameworks can be...
Decision Procedures for Inductive Boolean Functions based on Alternating Automata (2000)
Abdelwaheb Ayari, David Basin, Felix Klaedtke
. We show how alternating automata provide decision procedures for the equivalence of inductively dened Boolean functions that are useful for reasoning about parameterized families of circuits. We...
A Higher-Order Interpretation of Deductive Tableau (1999)
this paper may be found at http://www.informatik.uni-freiburg.de/¸ayari/dedtableau/. All system ouput given here is taken directly from an Isabelle session, with the exception of minor cosmetic...
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...
A Theoretical and Empirical Investigation of Search in Imperfect Information Games (1999)
We examine search algorithms for games with imperfect information. We first investigate Monte Carlo sampling, showing that for very simple game trees the chance of finding an optimal strategy rapidly...
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...
Lazy Infinite-State Analysis of Security Protocols (1999)
Security protocols are used to exchange information in a distributed system with the aim of providing security guarantees. We present an approach to modeling security protocols using lazy data types...
David Basin, Ian Frank, Ian Frank, Ian Frank
For many problem-solving tasks, it is important not only to produce solutions, but also to justify any solutions with explanations. In this paper, we describe how we are addressing this question...
A Higher-Order Interpretation of Deductive Tableau (1999)
this paper may be found at http://www.informatik.uni-freiburg.de/¸ayari/dedtableau/. All system ouput given here is taken directly from an Isabelle session, with the exception of minor cosmetic...
Optimal play against best defence: Complexity and heuristics (1998)
Abstract. We investigate the best defence model of an imperfect information game. In particular, we prove that finding optimal strategies for this model is NP-complete in the size of the game tree....
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...
LISA: A Specification Language Based on WS2S (1998)
Abdelwaheb Ayari, David Basin, Andreas Podelski
. We integrate two concepts from programming languages into a specification language based on WS2S, namely high-level data structures such as records and recursively-defined datatypes (WS2S is the...
Labelled Modal Logics: Quantifiers (1998)
David Basin, Seán Matthews, Luca Viganò
. In previous work we gave an approach, based on labelled natural deduction, for formalizing proof systems for a large class of propositional modal logics that includes K, D, T, B, S4, S4:2, KD45,...
Program Development Schemata as Derived Rules (1998)
This paper makes several contributions towards a clarified view of schema-based program development. First, we propose that schemata can be understood, formalized, and used in a simple way: program...
Labelled Modal Logics: Quantifiers (1998)
In previous work we gave an approach, based on labelled natural deduction, for formalizing proof systems for a large class of propositional modal logics that includes K, D, T, B, S4, S4:2, KD45, and...
LISA: A Specification Language Based on WS2S (1998)
Abdelwaheb Ayari, David Basin, Andreas Podelski
We integrate two concepts from programming languages into a specification language based on WS2S, namely high-level data structures such as records and recursively-defined datatypes (WS2S is the weak...
Search in Games with Incomplete Information: A Case Study using Bridge Card Play (1998)
We examine search algorithms in games with incomplete information, formalising a best defence model of such games based on the assumptions typically made when incomplete information problems are...
Automata Based Symbolic Reasoning in Hardware Verification (1998)
. We present a new approach to hardware verification based on describing circuits in Monadic Second-order Logic (M2L). We show how to use this logic to represent generic designs like n-bit adders,...
Automated Complexity Analysis Based on Ordered Resolution (1998)
David Basin, Harald Ganzinger, Im Stadtwald
We define order locality to be a property of clauses relative to a term ordering. This property is a kind of generalization of the subformula property for proofs where terms arising in proofs are...
Labelled Modal Logics: Quantifiers (1998)
David Basin, Seán Matthews, Luca Viganò
In previous work we gave an approach, based on labelled natural deduction, for formalizing proof systems for a large class of propositional modal logics that includes K, D, T, B, S4, S4:2, KD45, and...
Logical Framework Based Program Development (1998)
in the base theory. The use of a logical framework as opposed to, say, a theorem prover for first-order logic, is important here, as this step requires formalizing and reasoning about rules as...
Proof development systems traditionally structure theories hierarchically: Theorems established in a subtheory hold in all supertheories. While often eective, this is sometimes too restrictive as...
Optimal Play Against Best Defence: Complexity and Heuristics (1998)
. We investigate the best defence model of an imperfect information game. In particular, we prove that finding optimal strategies for this model is NP-complete in the size of the game tree. We then...
Formalization of the Development Process (1998)
David Basin, Bernd Krieg-Brückner
Introduction 14.1.1 What is development? Software development encompasses many phases including requirements engineering, specification, design, implementation, verification or testing, and...
Program Development Schemata as Derived Rules (1998)
this paper may be found on the web at http://www.tcnj.edu/¸penny/isalops. 1. Introduction
Ian Frank, David Basin, Hitoshi Matsubara
We investigate Monte-carlo sampling in games with imperfect information. We show that for very simple game trees the chance of finding the optimal strategy with Monte-carlo sampling rapidly...
Labelled Propositional Modal Logics: Theory and Practice (1997)
We show how labelled deductive systems can be combined with a logical framework to provide a natural deduction implementation of a large and well-known class of propositional modal logics (including...
A New Method for Bounding the Complexity of Modal Logics (1997)
David Basin, Seán Matthews, Luca Viganò
. We present a new proof-theoretic approach to bounding the complexity of the decision problem for propositional modal logics. We formalize logics in a uniform way as sequent systems and then...
Labelled Propositional Modal Logics: Theory and Practice (1997)
David Basin, Seán Matthews, Luca Viganò
We show how labelled deductive systems can be combined with a logical framework to provide a natural deduction implementation of a large and well-known class of propositional modal logics (including...
Labelled Propositional Modal Logics: Theory and Practice (1997)
BASIN, DAVID, MATTHEWS, SEÁN, VIGANÒ, LUCA
We show how labelled deductive systems can be combined with a logical framework to provide a natural deduction implementation of a large and well-known class of propositional modal logics (including...
Complexity Analysis Based on Ordered Resolution (1996)
We dene order locality to be a property of clauses relative to a term ordering. This property generalizes the subformula property for proofs where the terms appearing in proofs can be bounded, under...
Natural Deduction for Non-Classical Logics (1996)
David Basin, Sean Matthews, Luca Vigano, Im Stadtwald
We present a framework for machine implementation of families of non-classical logics with Kripke-style semantics. We decompose a logic into two interacting parts, each a natural deduction system: a...
Labelled Propositional Modal Logics: Theory and Practice (1996)
David Basin, Seán Matthews, Luca Viganò, Im Stadtwald
We show how labelled deductive systems can be combined with a logical framework to provide a natural deduction implementation of a large and well-known class of propositional modal logics (including...
Automated Complexity Analysis Based on Ordered Resolution (1996)
We define order locality to be a property of clauses relative to a term ordering. This property is a kind of generalization of the subformula property for proofs where the terms appearing in proofs...
Adding Metatheoretic Facilities to First-Order Theories (1996)
Generic proof systems like Isabelle provide some limited but useful metatheoretic facilities for declared logics; in particular, users can prove simple derived rules and also `solve' formulae...
Formal Software Engineering (1996)
, VDM and Z. A brief introduction to the sort of mathematical concepts these languages are based on, and the sorts of problems they can formalise, can be found in the tutorial articles on Z by Hayes...
Search in Games with Incomplete Information: A Case Study using Bridge Card Play (1996)
Study Bridge, Card Play, Ian Frank, Ian Frank, David Basin, David Basin
We examine search algorithms in games with incomplete information. We proceed by adopting the standard game theoretic framework of zero-sum two-player games, introducing a reduced form of incomplete...
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...
Natural Deduction for Non-Classical Logics (1996)
We present a framework for machine implementation of families of non-classical logics with Kripke-style semantics. We decompose a logic into two interacting parts, each a natural deduction system: a...
Structuring Metatheory on Inductive Definitions (1996)
David Basin, Seán Matthews, Im Stadtwald
We examine a problem in formal metatheory: if theories are structured hierarchically, there are metatheorems which hold in only some extensions. We illustrate this using modal logics and the...
Implementing Modal and Relevance Logics in a Logical Framework (1996)
We present a framework for machine implementation of both partial and complete fragments of large families of non-classical logics such as modal, relevance, and intuitionistic logics. We decompose a...
Experiments in Automating Hardware Verification using Inductive Proof Planning (1996)
Francisco J. Cantu, Alan Bundy, Alan Smaill, David Basin
. We present a new approach to automating the verification of hardware designs based on planning techniques. A database of methods is developed that combines tactics, which construct proofs, using...
Implementing Modal and Relevance Logics in a Logical Framework (1996)
David Basin, Seán Matthews, Luca Viganò, Im Stadtwald
We present a framework for machine implementation of both partial and complete fragments of large families of non-classical logics such as modal, relevance, and intuitionistic logics. We decompose a...
Complexity Analysis Based on Ordered Resolution (1996)
We define order locality to be a property of clauses relative to a term ordering. This property is a kind of generalization of the subformula property for proofs where terms arising in proofs are...
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...
Natural Deduction for Non-Classical Logics (1996)
David Basin, Seán Matthews, Luca Viganò
We present a framework for machine implementation of families of non-classical logics with Kripke-style semantics. We decompose a logic into two interacting parts, each a natural deduction system: a...
Complexity Analysis Based on Ordered Resolution (1996)
We define order locality to be a property of clauses relative to a term ordering. This property is a kind of generalization of the subformula property for proofs where terms arising in proofs are...
Adding Metatheoretic Facilities to First-order Theories (1996)
Generic proof systems like Isabelle provide some limited but useful metatheoretic facilities for declared logics; in particular, users can prove simple derived rules and also ‘solve’ formulae...
Deriving and Applying Logic Program Transformers (1995)
We present a methodology for logic program development based on the use of verified transformation templates. We use the Isabelle Logical Framework to formalize transformation templates as inference...
Middle-Out Reasoning for Synthesis and Induction (1995)
Ina Kraan, David Basin, Alan Bundy
We develop two applications of middle-out reasoning in inductive proofs: Logic program synthesis and the selection of induction schemes. Middleout reasoning as part of proof planning was first...
Induction Based on Rippling and Proof Planning Part I: Rippling and Proof Planning (1994)
David Basin, Mpi Saarbrucken, David Basin
Notes Series. Copies may be obtained by contacting:
Logic Program Synthesis via Proof Planning (1993)
Ina Kraan, Ina Kraan, David Basin, David Basin, David Basin, ...
We propose a novel approach to automating the synthesis of logic programs: Logic programs are synthesized as a by-product of the planning of a verification proof. The approach is a two-level one: At...
Middle-Out Reasoning for Logic Program Synthesis (1993)
Ina Kraan David, Ina Kraan, David Basin, David Basin, David Basin, ...
We propose a novel approach to automating the synthesis of logic programs: Logic programs are synthesized as a by-product of the planning of a verification proof. The approach is a two-level one: At...
Natural Deduction for Non-Classical Logics (1993)
David Basin, Sean Matthews, Luca Vigano
We present a framework for machine implementation of families of non-classical logics with Kripke-style semantics. We decompose a logic into two interacting parts, each a natural deduction system: a...
Experience with FS 0 as a framework theory (1993)
Sean Matthews, Alan Smaill, David Basin
Feferman has proposed a system, FS 0 , as an alternative framework for encoding logics and also for reasoning about those encodings. We have implemented a version of this framework and performed...
Middle-Out Reasoning for Logic Program Synthesis (1993)
Im Stadtwald, Ina Kraan, Ina Kraan, David Basin, David Basin, Alan Bundy, ...
Logic programs can be synthesized as a by-product of the planning of their verification proofs. This is achieved by using higher-order variables at the proof planning level, which become instantiated...
A Framework for Program Development Based on Schematic Proof (1993)
David Basin, Alan Bundy, Ina Kraan, Sean Matthews, Im Stadtwald
. Often, calculi for manipulating and reasoning about programs can be recast as calculi for synthesizing programs. The difference involves often only a slight shift of perspective: admitting...
An Adaptation of Proof-Planning to Declarer Play in Bridge (1992)
In Bridge, Ian Frank, David Basin, Alan Bundy
. We present Finesse, a system that forms plans for declarer play in the game of Bridge. Finesse generalises the technique of proof-planning, developed at Edinburgh University in the context of...
An Adaptation of Proof-Planning to Declarer Play in Bridge (1992)
Ian Frank, David Basin, Alan Bundy
. We present Finesse, a system that forms optimal plans for declarer play in the game of Bridge. Finesse generalises the technique of proof-planning, developed at Edinburgh University in the context...
David Basin, Im Stadtwald, Im Stadtwald, Toby Walsh, Toby Walsh
We extend previous work on difference identification and reduction as a technique for automated reasoning. We generalize unification so that terms are made equal not only by finding substitutions for...
A Recursion Planning Analysis of Inductive Completion (1992)
Richard Barnett, David Basin, Jane Hesketh
We use the AI proof planning techniques of recursion analysis and rippling as tools to analyze so called inductionless induction proof techniques. Recursion analysis chooses induction schemas and...
Automating Meta-Theory Creation and System Extension (1991)
David Basin, Fausto Giunchiglia, Paolo Traverso
In this paper we describe a first experiment with a new approach for building theorem provers that can formalize themselves, reason about themselves, and safely extend themselves with new inference...
The Boyer-Moore Prover and Nuprl: An Experimental Comparison (1991)
We use an example to compare the Boyer-Moore Theorem Prover and the Nuprl Proof Development System. The respective machine verifications of a version of Ramsey's theorem illustrate similarities...
Some Normalization Properties of Martin-Lof's Type Theory, and Applications (1991)
For certain kinds of applications of type theories, the faithfulness of formalization in the theory depends on intensional, or structural, properties of objects constructed in the theory. For type...
Rewriting logic as a metalogical framework (1974)
A metalogical framework is a logic with an associated methodology that is used to represent other logics and to reason about their metalogical properties. We propose that logical frameworks can be...
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...
Middle-Out Reasoning for Synthesis and Induction
David Basin, David Basin, Ina Kraan David, Ina Kraan, Alan Bundy, ...
We develop two applications of middle-out reasoning in inductive proofs: Logic program synthesis and the selection of induction schemes. Middle-out reasoning as part of proof planning was first...
A Topography Of Labelled Modal Logics
David Basin, An Matthews, Luca Vigan
. Labelled Deductive Systems provide a general method for representing logics in a modular and transparent way. A Labelled Deductive System consists of two parts, a base logic and a labelling...
Labelled Quantified Modal Logics
David Basin, Sean Matthews, Luca Vigano
. We present an approach to providing natural deduction style proof systems for a large class of quantified modal logics with varying, increasing, decreasing or constant domains of quantification....
A Topography Of Labelled Modal Logics
David Basin, Seán Matthews, Luca Viganò
. Labelled Deductive Systems provide a general method for representing logics in a modular and transparent way. A Labelled Deductive System consists of two parts, a base logic and a labelling...
A Modular Presentation of Modal Logics in a Logical Framework
David Basin, Seán Matthews, Luca Viganò
We present a theoretical and practical approach to the modular natural deduction presentation of modal logics and their implementation in a logical framework. Our work treats a large and well-known...
A Modular Presentation of Modal Logics in a Logical Framework
David Basin, Seán Matthews, Luca Viganò
We present a theoretical and practical approach to the modular natural deduction presentation of modal logics and their implementation in a logical framework. Our work treats a large and well-known...