David A. Basin

According to our database1, David A. Basin authored at least 238 papers between 1988 and 2018.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepages:

On csauthors.net:

Bibliography

2018
Model Checking Security Protocols.
Proceedings of the Handbook of Model Checking., 2018

Design, Analysis, and Implementation of ARPKI: An Attack-Resilient Public-Key Infrastructure.
IEEE Trans. Dependable Sec. Comput., 2018

Refining security protocols.
Journal of Computer Security, 2018

From Natural Projection to Partial Model Checking and Back.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018

Scalable Online First-Order Monitoring.
Proceedings of the Runtime Verification - 18th International Conference, 2018

Networking in Heaven as on Earth.
Proceedings of the 17th ACM Workshop on Hot Topics in Networks, 2018

Mining ABAC Rules from Sparse Logs.
Proceedings of the 2018 IEEE European Symposium on Security and Privacy, 2018

Alethea: A Provably Secure Random Sample Voting Protocol.
Proceedings of the 31st IEEE Computer Security Foundations Symposium, 2018

A Formal Analysis of 5G Authentication.
Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, 2018

Optimal Proofs for Linear Temporal Logic on Lasso Words.
Proceedings of the Automated Technology for Verification and Analysis, 2018

2017
Symbolically analyzing security protocols using tamarin.
SIGLOG News, 2017

CryptHOL: Game-based Proofs in Higher-order Logic.
IACR Cryptology ePrint Archive, 2017

Election Security and Economics: It's All About Eve.
Proceedings of the Electronic Voting - Second International Joint Conference, 2017

Almost Event-Rate Independent Monitoring of Metric Temporal Logic.
Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

The MonPoly Monitoring Tool.
Proceedings of the RV-CuBES 2017. An International Workshop on Competitions, 2017

AERIAL: Almost Event-Rate Independent Algorithms for Monitoring Metric Regular Properties.
Proceedings of the RV-CuBES 2017. An International Workshop on Competitions, 2017

Almost Event-Rate Independent Monitoring of Metric Dynamic Logic.
Proceedings of the Runtime Verification - 17th International Conference, 2017

Test execution checkpointing for web applications.
Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, Santa Barbara, CA, USA, July 10, 2017

Refining Authenticated Key Agreement with Strong Adversaries.
Proceedings of the 2017 IEEE European Symposium on Security and Privacy, 2017

Securing Databases from Probabilistic Inference.
Proceedings of the 30th IEEE Computer Security Foundations Symposium, 2017

Cutoff Bounds for Consensus Algorithms.
Proceedings of the Computer Aided Verification - 29th International Conference, 2017

Runtime Verification of Temporal Properties over Out-of-Order Data Streams.
Proceedings of the Computer Aided Verification - 29th International Conference, 2017

Tests and Refutation.
Proceedings of the Automated Technology for Verification and Analysis, 2017

2016
Large-scale system development using Abstract Data Types and refinement.
Sci. Comput. Program., 2016

Scalable offline monitoring of temporal specifications.
Formal Methods in System Design, 2016

Strong and Provably Secure Database Access Control.
Proceedings of the IEEE European Symposium on Security and Privacy, 2016

Security Testing Beyond Functional Tests.
Proceedings of the Engineering Secure Software and Systems - 8th International Symposium, 2016

Access Control Synthesis for Physical Spaces.
Proceedings of the IEEE 29th Computer Security Foundations Symposium, 2016

Modeling Human Errors in Security Protocols.
Proceedings of the IEEE 29th Computer Security Foundations Symposium, 2016

In the Nick of Time: Proactive Prevention of Obligation Violations.
Proceedings of the IEEE 29th Computer Security Foundations Symposium, 2016

2015
Monitoring Metric First-Order Temporal Properties.
J. ACM, 2015

Greedily computing associative aggregations on sliding windows.
Inf. Process. Lett., 2015

Improving the Security of Cryptographic Protocol Standards.
IEEE Security & Privacy, 2015

Semantic Vacuity.
Proceedings of the 22nd International Symposium on Temporal Representation and Reasoning, 2015

Failure-aware Runtime Verification of Distributed Systems.
Proceedings of the 35th IARCS Annual Conference on Foundation of Software Technology and Theoretical Computer Science, 2015

Consensus Refined.
Proceedings of the 45th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, 2015

Analyzing First-Order Role Based Access Control.
Proceedings of the IEEE 28th Computer Security Foundations Symposium, 2015

A Complete Characterization of Secure Human-Server Communication.
Proceedings of the IEEE 28th Computer Security Foundations Symposium, 2015

Automated Symbolic Proofs of Observational Equivalence.
Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, 2015

Alice and Bob Meet Equational Theories.
Proceedings of the Logic, Rewriting, and Concurrency, 2015

2014
Model-Driven Development of a Secure eHealth Application.
Proceedings of the Engineering Secure Future Internet Services and Systems, 2014

A Model-Driven Methodology for Developing Secure Data-Management Applications.
IEEE Trans. Software Eng., 2014

Know Your Enemy: Compromising Adversaries in Protocol Analysis.
ACM Trans. Inf. Syst. Secur., 2014

Optimal Security-Aware Query Processing.
PVLDB, 2014

Obstruction-free authorization enforcement: Aligning security and business objectives.
Journal of Computer Security, 2014

LTL is closed under topological closure.
Inf. Process. Lett., 2014

Deciding safety and liveness in TPTL.
Inf. Process. Lett., 2014

On Secure Data Deletion.
IEEE Security & Privacy, 2014

Short paper: detection of GPS spoofing attacks in power grids.
Proceedings of the 7th ACM Conference on Security & Privacy in Wireless and Mobile Networks, 2014

Automated Verification of Group Key Agreement Protocols.
Proceedings of the 2014 IEEE Symposium on Security and Privacy, 2014

On Real-Time Monitoring with Imprecise Timestamps.
Proceedings of the Runtime Verification - 5th International Conference, 2014

Scalable Offline Monitoring.
Proceedings of the Runtime Verification - 5th International Conference, 2014

Decentralized Composite Access Control.
Proceedings of the Principles of Security and Trust - Third International Conference, 2014

Code Generation for Event-B.
Proceedings of the Integrated Formal Methods - 11th International Conference, 2014

Anchored LTL separation.
Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 2014

Actor Key Compromise: Consequences and Countermeasures.
Proceedings of the IEEE 27th Computer Security Foundations Symposium, 2014

Fail-Secure Access Control.
Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, 2014

ARPKI: Attack Resilient Public-Key Infrastructure.
Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, 2014

Formal System Modelling Using Abstract Data Types in Event-B.
Proceedings of the Abstract State Machines, Alloy, B, TLA, VDM, and Z, 2014

2013
Monitoring Data Usage in Distributed Systems.
IEEE Trans. Software Eng., 2013

Predictable Mobile Routing for Spacecraft Networks.
IEEE Trans. Mob. Comput., 2013

Role Mining with Probabilistic Models.
ACM Trans. Inf. Syst. Secur., 2013

Efficient construction of machine-checked symbolic protocol security proofs.
Journal of Computer Security, 2013

SoK: Secure Data Deletion.
Proceedings of the 2013 IEEE Symposium on Security and Privacy, 2013

Monitoring of Temporal First-Order Properties with Aggregations.
Proceedings of the Runtime Verification - 4th International Conference, 2013

Semi-valid input coverage for fuzz testing.
Proceedings of the International Symposium on Software Testing and Analysis, 2013

Symbolic Probabilistic Analysis of Off-Line Guessing.
Proceedings of the Computer Security - ESORICS 2013, 2013

Secure data deletion from persistent media.
Proceedings of the 2013 ACM SIGSAC Conference on Computer and Communications Security, 2013

The TAMARIN Prover for the Symbolic Analysis of Security Protocols.
Proceedings of the Computer Aided Verification - 25th International Conference, 2013

Technology Transfer.
Proceedings of the Industrial Deployment of System Engineering Methods, 2013

2012
Multi-Assignment Clustering for Boolean Data.
Journal of Machine Learning Research, 2012

The research value of publishing attacks.
Commun. ACM, 2012

Data Node Encrypted File System: Efficient Secure Deletion for Flash Memory.
Proceedings of the 21th USENIX Security Symposium, Bellevue, WA, USA, August 8-10, 2012, 2012

Optimal workflow-aware authorizations.
Proceedings of the 17th ACM Symposium on Access Control Models and Technologies, 2012

Monitoring Compliance Policies over Incomplete and Disagreeing Logs.
Proceedings of the Runtime Verification, Third International Conference, 2012

Enforceable Security Policies Revisited.
Proceedings of the Principles of Security and Trust - First International Conference, 2012

Provably Repairing the ISO/IEC 9798 Standard for Entity Authentication.
Proceedings of the Principles of Security and Trust - First International Conference, 2012

SECFUZZ: Fuzz-testing security protocols.
Proceedings of the 7th International Workshop on Automation of Software Test, 2012

Refining Key Establishment.
Proceedings of the 25th IEEE Computer Security Foundations Symposium, 2012

Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties.
Proceedings of the 25th IEEE Computer Security Foundations Symposium, 2012

User-level secure deletion on log-structured file systems.
Proceedings of the 7th ACM Symposium on Information, Compuer and Communications Security, 2012

2011
Formal Reasoning about Physical Properties of Security Protocols.
ACM Trans. Inf. Syst. Secur., 2011

Distributed temporal logic for the analysis of security protocol models.
Theor. Comput. Sci., 2011

Automatically deriving information-theoretic bounds for adaptive side-channel attacks.
Journal of Computer Security, 2011

Monitoring Usage-Control Policies in Distributed Systems.
Proceedings of the Eighteenth International Symposium on Temporal Representation and Reasoning, 2011

A decade of model-driven security.
Proceedings of the 16th ACM Symposium on Access Control Models and Technologies, 2011

Algorithms for Monitoring Real-Time Properties.
Proceedings of the Runtime Verification - Second International Conference, 2011

MONPOLY: Monitoring Usage-Control Policies.
Proceedings of the Runtime Verification - Second International Conference, 2011

FAST: An Efficient Decision Procedure for Deduction and Static Equivalence.
Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, 2011

Constructing Mid-Points for Two-Party Asynchronous Protocols.
Proceedings of the Principles of Distributed Systems - 15th International Conference, 2011

Model-Driven Development of Security-Aware GUIs for Data-Centric Applications.
Proceedings of the Foundations of Security Analysis and Design VI, 2011

Obstruction-Free Authorization Enforcement: Aligning Security with Business Objectives.
Proceedings of the 24th IEEE Computer Security Foundations Symposium, 2011

Separation of duties as a service.
Proceedings of the 6th ACM Symposium on Information, Computer and Communications Security, 2011

Applied Information Security - a Hands-on Approach.
Springer, ISBN: 978-3-642-24473-5, 2011

2010
Efficient analysis of pattern-based constraint specifications.
Software and System Modeling, 2010

Constraint differentiation: Search-space reduction for the constraint-based analysis of security protocols.
Journal of Computer Security, 2010

On the definition of role mining.
Proceedings of the 15th ACM Symposium on Access Control Models and Technologies, 2010

Monitoring security policies with metric first-order temporal logic.
Proceedings of the 15th ACM Symposium on Access Control Models and Technologies, 2010

Efficient Decision Procedures for Message Deducibility and Static Equivalence.
Proceedings of the Formal Aspects of Security and Trust - 7th International Workshop, 2010

SSG: a model-based development environment for smart, security-aware GUIs.
Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering, 2010

How to Evaluate the Security of Real-Life Cryptographic Protocols? - The Cases of ISO/IEC 29128 and CRYPTREC.
Proceedings of the Financial Cryptography and Data Security, 2010

Automatic Generation of Smart, Security-Aware GUI Models.
Proceedings of the Engineering Secure Software and Systems, Second International Symposium, 2010

Modeling and Analyzing Security in the Presence of Compromising Adversaries.
Proceedings of the Computer Security, 2010

Degrees of Security: Protocol Guarantees in the Face of Compromising Adversaries.
Proceedings of the Computer Science Logic, 24th International Workshop, 2010

Impossibility Results for Secret Establishment.
Proceedings of the 23rd IEEE Computer Security Foundations Symposium, 2010

Strong Invariants for the Efficient Construction of Machine-Checked Protocol Security Proofs.
Proceedings of the 23rd IEEE Computer Security Foundations Symposium, 2010

Developing security protocols by refinement.
Proceedings of the 17th ACM Conference on Computer and Communications Security, 2010

Policy Monitoring in First-Order Temporal Logic.
Proceedings of the Computer Aided Verification, 22nd International Conference, 2010

Keeping data secret under full compromise using porter devices.
Proceedings of the Twenty-Sixth Annual Computer Security Applications Conference, 2010

2009
Labelled Tableaux for Distributed Temporal Logic.
J. Log. Comput., 2009

Automated analysis of security-design models.
Information & Software Technology, 2009

From Dolev-Yao to Strong Adaptive Corruption: Analyzing Security in the Presence of Compromising Adversaries.
IACR Cryptology ePrint Archive, 2009

Let's Get Physical: Models and Methods for Real-World Security Protocols.
Proceedings of the Theorem Proving in Higher Order Logics, 22nd International Conference, 2009

Developing Topology Discovery in Event-B.
Proceedings of the Integrated Formal Methods, 7th International Conference, 2009

Multi-assignment clustering for Boolean data.
Proceedings of the 26th Annual International Conference on Machine Learning, 2009

Dynamic Enforcement of Abstract Separation of Duty Constraints.
Proceedings of the Computer Security, 2009

Modeling and Verifying Physical Properties of Security Protocols for Wireless Networks.
Proceedings of the 22nd IEEE Computer Security Foundations Symposium, 2009

A probabilistic approach to hybrid role mining.
Proceedings of the 2009 ACM Conference on Computer and Communications Security, 2009

2008
SSL/TLS Session-Aware User Authentication.
IEEE Computer, 2008

SSL/TLS session-aware user authentication revisited.
Computers & Security, 2008

Secure neighborhood discovery: a fundamental element for mobile ad hoc networking.
IEEE Communications Magazine, 2008

Two approaches to an information security laboratory.
Commun. ACM, 2008

A Labeled Tableaux Systemfor the Distributed Temporal Logic DTL.
Proceedings of the 15th International Symposium on Temporal Representation and Reasoning, 2008

Topology dynamics and routing for predictable mobile networks.
Proceedings of the 16th annual IEEE International Conference on Network Protocols, 2008

Runtime Monitoring of Metric First-order Temporal Properties.
Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2008

Cryptographically-Sound Protocol-Model Abstractions.
Proceedings of the 21st IEEE Computer Security Foundations Symposium, 2008

Mechanisms for usage control.
Proceedings of the 2008 ACM Symposium on Information, Computer and Communications Security, 2008

A class of probabilistic models for role engineering.
Proceedings of the 2008 ACM Conference on Computer and Communications Security, 2008

2007
Preface.
Journal of Computer Security, 2007

Verifying a signature architecture: a comparative case study.
Formal Asp. Comput., 2007

Securing the Distribution and Storage of Secrets with Trusted Platform Modules.
Proceedings of the Information Security Theory and Practices. Smart Cards, 2007

A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols.
Proceedings of the Theorem Proving in Higher Order Logics, 20th International Conference, 2007

A Metamodel-Based Approach for Analyzing Security-Design Models.
Proceedings of the Model Driven Engineering Languages and Systems, 2007

A Proof of Concept Implementation of SSL/TLS Session-Aware User Authentication (TLS-SA).
Proceedings of the Kommunikation in Verteilten Systemen (KiVS), 2007

Monitors for Usage Control.
Proceedings of the Trust Management, 2007

A Policy Language for Distributed Usage Control.
Proceedings of the Computer Security, 2007

An information-theoretic model for adaptive side-channel attacks.
Proceedings of the 2007 ACM Conference on Computer and Communications Security, 2007

Specifying and analyzing security automata using CSP-OZ.
Proceedings of the 2007 ACM Symposium on Information, Computer and Communications Security, 2007

BAP: Broadcast Authentication Using Cryptographic Puzzles.
Proceedings of the Applied Cryptography and Network Security, 5th International Conference, 2007

Midpoints Versus Endpoints: From Protocols to Firewalls.
Proceedings of the Applied Cryptography and Network Security, 5th International Conference, 2007

2006
Model driven security: From UML models to access control infrastructures.
ACM Trans. Softw. Eng. Methodol., 2006

On the semantics of Alice&Bob specifications of security protocols.
Theor. Comput. Sci., 2006

Automated Reasoning for Security Protocol Analysis.
J. Autom. Reasoning, 2006

SSL/TLS session-aware user authentication - Or how to effectively thwart the man-in-the-middle.
Computer Communications, 2006

Distributed usage control.
Commun. ACM, 2006

Formalizing and Analyzing Sender Invariance.
Proceedings of the Formal Aspects in Security and Trust, Fourth International Workshop, 2006

Controlling Access to Documents: A Formal Access Control Model.
Proceedings of the Emerging Trends in Information and Communication Security, 2006

Timing-Sensitive Information Flow Analysis for Synchronous Systems.
Proceedings of the Computer Security, 2006

Cryptographically Sound Theorem Proving.
Proceedings of the 19th IEEE Computer Security Foundations Workshop, 2006

Model Driven Security.
Proceedings of the The First International Conference on Availability, 2006

2005
Konflikt oder Review zwei Ansätze für Labors in angewandter Informationssicherheit.
Informatik Spektrum, 2005

OFMC: A symbolic model checker for security protocols.
Int. J. Inf. Sec., 2005

Relating Strand Spaces and Distributed Temporal Logic for Security Protocol Analysis.
Logic Journal of the IGPL, 2005

Deconstructing Alice and Bob.
Electr. Notes Theor. Comput. Sci., 2005

Metareasoning about Security Protocols using Distributed Temporal Logic.
Electr. Notes Theor. Comput. Sci., 2005

Firewall Conformance Testing.
Proceedings of the Testing of Communicating Systems, 2005

Algebraic Intruder Deductions.
Proceedings of the Logic for Programming, 2005

Verification of a Signature Architecture with HOL-Z.
Proceedings of the FM 2005: Formal Methods, 2005

On Obligations.
Proceedings of the Computer Security, 2005

The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications.
Proceedings of the Computer Aided Verification, 17th International Conference, 2005

2004
Reflective metalogical frameworks.
ACM Trans. Comput. Log., 2004

Editorial.
Higher-Order and Symbolic Computation, 2004

Synthesis of Programs in Computational Logic.
Proceedings of the Program Development in Computational Logic: A Decade of Research Advances in Logic-Based Program Development, 2004

2003
Bytecode Verification by Model Checking.
J. Autom. Reasoning, 2003

A Formal Analysis of a Digital Signature Architecture.
Proceedings of the Integrity and Internal Control in Information Systems VI, 2003

Model driven security for process-oriented systems.
Proceedings of the 8th ACM Symposium on Access Control Models and Technologies, 2003

An On-the-Fly Model-Checker for Security Protocol Analysis.
Proceedings of the Computer Security, 2003

CDiff: a new reduction technique for constraint-based analysis of security protocols.
Proceedings of the 10th ACM Conference on Computer and Communications Security, 2003

2002
A Formal Analysis of the CORBA Security Service.
Proceedings of the ZB 2002: Formal Specification and Development in Z and B, 2002

SecureUML: A UML-Based Modeling Language for Model-Driven Security.
Proceedings of the UML 2002 - The Unified Modeling Language, 5th International Conference, Dresden, Germany, September 30, 2002

Verified Bytecode Model Checkers.
Proceedings of the Theorem Proving in Higher Order Logics, 15th International Conference, 2002

Bytecode Model Checking: An Experimental Analysis.
Proceedings of the Model Checking of Software, 2002

QUBOS: Deciding Quantified Boolean Logic Using Propositional Satisfiability Solvers.
Proceedings of the Formal Methods in Computer-Aided Design, 4th International Conference, 2002

The Next 700 Synthesis Calculi.
Proceedings of the FME 2002: Formal Methods, 2002

The AVISS Security Protocol Analysis Tool.
Proceedings of the Computer Aided Verification, 14th International Conference, 2002

2001
A theoretical and empirical investigation of search in imperfect information games.
Theor. Comput. Sci., 2001

A Higher-order Interpretation of Deductive Tableau.
J. Symb. Comput., 2001

Current Trends in Logical Frameworks and Metalanguages.
J. Autom. Reasoning, 2001

Automated complexity analysis based on ordered resolution.
J. ACM, 2001

Towards an awareness-based semantics for security protocol analysis.
Electr. Notes Theor. Comput. Sci., 2001

A formal data-model of the CORBA security service.
Proceedings of the 8th European Software Engineering Conference held jointly with 9th ACM SIGSOFT International Symposium on Foundations of Software Engineering 2001, 2001

2000
Program Development Schemata as Derived Rules.
J. Symb. Comput., 2000

Maude versus Haskell: an Experimental Comparison in Security Protocol Analysis.
Electr. Notes Theor. Comput. Sci., 2000

Rewriting Logic as a Metalogical Framework.
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 2000

B2M: A Semantic Based Tool for BLIF Hardware Descriptions.
Proceedings of the Formal Methods in Computer-Aided Design, Third International Conference, 2000

Decision Procedures for Inductive Boolean Functions Based on Alternating Automata.
Proceedings of the Computer Aided Verification, 12th International Conference, 2000

Bounded Model Construction for Monadic Second-Order Logics.
Proceedings of the Computer Aided Verification, 12th International Conference, 2000

Combining Knowledge and Search to Solve Single-Suit Bridge.
Proceedings of the Seventeenth National Conference on Artificial Intelligence and Twelfth Conference on on Innovative Applications of Artificial Intelligence, July 30, 2000

1999
Formalization of the Development Process.
Proceedings of the Algebraic Foundations of Systems Specification, 1999

Structural and Behavioral Modeling with Monadic Logics.
Proceedings of the 29th IEEE International Symposium on Multiple-Valued Logic, 1999

Lazy Infinite-State Analysis of Security Protocols.
Proceedings of the Secure Networking - CQRE (Secure) '99, International Exhibition and Congress Düsseldorf, Germany, November 30, 1999

Java Bytecode Verification by Model Checking.
Proceedings of the Computer Aided Verification, 11th International Conference, 1999

1998
Natural Deduction for Non-Classical Logics.
Studia Logica, 1998

Labelled Modal Logics: Quantifiers.
Journal of Logic, Language and Information, 1998

Search in Games with Incomplete Information: A Case Study Using Bridge Card Play.
ICGA Journal, 1998

Scoped metatheorems.
Electr. Notes Theor. Comput. Sci., 1998

Logical-Framework-Based Program Development.
ACM Comput. Surv., 1998

Search in Games with Incomplete Information: A Case Study Using Bridge Card Play.
Artif. Intell., 1998

Optimal Play against Best Defence: Complexity and Heuristics.
Proceedings of the Computers and Games, First International Conference, 1998

Finding Optimal Strategies for Imperfect Information Games.
Proceedings of the Fifteenth National Conference on Artificial Intelligence and Tenth Innovative Applications of Artificial Intelligence Conference, 1998

1997
Labelled Propositional Modal Logics: Theory and Practice.
J. Log. Comput., 1997

Labelled Quantified Modal Logics.
Proceedings of the KI-97: Advances in Artificial Intelligence, 1997

A New Method for Bounding the Complexity of Modal Logics.
Proceedings of the Computational Logic and Proof Theory, 5th Kurt Gödel Colloquium, 1997

LISA: A Specification Language Based on WS2S.
Proceedings of the Computer Science Logic, 11th International Workshop, 1997

1996
Adding Metatheoretic Facilities to First-Order Theories.
J. Log. Comput., 1996

Middle-Out Reasoning for Synthesis and Induction.
J. Autom. Reasoning, 1996

A Calculus for and Termination of Rippling.
J. Autom. Reasoning, 1996

Modeling a Hardware Synthesis Methodology in Isabelle.
Proceedings of the Theorem Proving in Higher Order Logics, 9th International Conference, 1996

Generic System Support for Deductive Program Development.
Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 1996

Complexity Analysis Based on Ordered Resolution.
Proceedings of the Proceedings, 1996

Implementing Modal and Relevance Logics in a Logical Framework.
Proceedings of the Fifth International Conference on Principles of Knowledge Representation and Reasoning (KR'96), 1996

A Topography of Labelled Modal Logics.
Proceedings of the Frontiers of Combining Systems, 1996

Experiments in Automating Hardware Verification Using Inductive Proof Planning.
Proceedings of the Formal Methods in Computer-Aided Design, First International Conference, 1996

Structuring Metatheory on Inductive Definitions.
Proceedings of the Automated Deduction - CADE-13, 13th International Conference on Automated Deduction, New Brunswick, NJ, USA, July 30, 1996

1995
Hardware Verification using Monadic Second-Order Logic.
Proceedings of the Computer Aided Verification, 1995

Deriving and Applying Logic Program Transformers.
Proceedings of the Algorithms, 1995

1994
A Term Equality Problem Equivalent to Graph Isomorphism.
Inf. Process. Lett., 1994

Generalized Rewriting in Type Theory.
Elektronische Informationsverarbeitung und Kybernetik, 1994

Logic Frameworks for Logic Programs.
Proceedings of the Logic Programming Synthesis and Transformation, 1994

IsaWhelk Interpreted in Isabelle.
Proceedings of the Logic Programming, 1994

Coloured Rippling: An Extension of a Theorem Proving Heuristic.
ECAI, 1994

A Calculus for Rippling.
Proceedings of the Conditional and Typed Rewriting Systems, 4th International Workshop, 1994

Termination Orderings for Rippling.
Proceedings of the Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26, 1994

1993
A Recursion Planning Analysis of Inductive Completion.
Ann. Math. Artif. Intell., 1993

A Framework for Program Development Based on Schematic Proof.
Proceedings of the 7th International Workshop on Software Specification and Design, 1993

Difference Unification.
Proceedings of the 13th International Joint Conference on Artificial Intelligence. Chambéry, France, August 28, 1993

Middle-Out Reasoning for Logic Program Synthesis.
Proceedings of the Logic Programming, 1993

A Conservative Extension of First-order Logic and Its Application to Theorem Proving.
Proceedings of the Foundations of Software Technology and Theoretical Computer Science, 1993

1992
Logic Program Synthesis via Proof Planning.
Proceedings of the Logic Program Synthesis and Transformation, 1992

An Adaptation of Proof-Planning to Declarer Play in Bridge.
ECAI, 1992

Difference Matching.
Proceedings of the Automated Deduction, 1992

1991
Formally verified synthesis of combinational CMOS circuits.
Integration, 1991

Some Normalization Properties of Martin-Löf's Type Theory, and Applications.
Proceedings of the Theoretical Aspects of Computer Software, 1991

Automating Meta-Theory Creation and System Extension.
Proceedings of the Trends in Artificial Intelligence, 1991

1990
Equality of Terms Containing Associative-Commutative Functions and Commutative Binding Operators in Isomorphism Complete.
Proceedings of the 10th International Conference on Automated Deduction, 1990

1989
Verification Of Combinational Logic in Nuprl.
Proceedings of the Hardware Specification, 1989

Building Theories in Nuprl.
Proceedings of the Logic at Botik '89, 1989

1988
An Environment For Automated Reasoning About Partial Functions.
Proceedings of the 9th International Conference on Automated Deduction, 1988


  Loading...