Konrad Slind

According to our database, Konrad Slind authored at least 53 papers between 1987 and 2023.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of three.

2023

Synthesizing verified components for cyber assured systems engineering.

Eric Mercer, Konrad Slind, Isaac Amundson, Darren D. Cofer, Junaid Babar, David S. Hardin

Softw. Syst. Model., October, 2023

Model-driven development for the seL4 microkernel using the HAMR framework.

Jason Belt, John Hatcliff, Robby, John Shackleton, Jim Carciofini, Todd Carpenter, Eric Mercer, Isaac Amundson, Junaid Babar, Darren D. Cofer, David S. Hardin, Karl Hoech, Konrad Slind, Ihor Kuz, Kent McLeod

J. Syst. Archit., 2023

2022

Cyberassured Systems Engineering at Scale.

Darren D. Cofer, Isaac Amundson, Junaid Babar, David S. Hardin, Konrad Slind, Perry Alexander, John Hatcliff, Robby, Gerwin Klein, Corey Lewis, Eric Mercer, John Shackleton

IEEE Secur. Priv., 2022

2021

Formal Synthesis of Filter Components for Use in Security-Enhancing Architectural Transformations.

David S. Hardin, Konrad L. Slind

Proceedings of the IEEE Security and Privacy Workshops, 2021

Specifying Message Formats with Contiguity Types.

Konrad Slind

Proceedings of the 12th International Conference on Interactive Theorem Proving, 2021

2018

Using ACL2 in the Design of Efficient, Verifiable Data Structures for High-Assurance Systems.

David S. Hardin, Konrad Slind

Proceedings of the 15th International Workshop on the ACL2 Theorem Prover and Its Applications, 2018

2017

Qualification of a Model Checker for Avionics Software Verification.

Lucas G. Wagner, Alain Mebsout, Cesare Tinelli, Darren D. Cofer, Konrad Slind

Proceedings of the NASA Formal Methods - 9th International Symposium, 2017

2016

A High-Assurance, High-Performance Hardware-Based Cross-Domain System.

David S. Hardin, Konrad Slind, Mark Bortz, James Potts, Scott Owens

Proceedings of the Computer Safety, Reliability, and Security, 2016

2015

Qualification of Formal Methods Tools (Dagstuhl Seminar 15182).

Darren D. Cofer, Gerwin Klein, Konrad Slind, Virginie Wiels

Dagstuhl Reports, 2015

2014

Resolute: an assurance case language for architecture models.

Andrew Gacek, John Backes, Darren D. Cofer, Konrad Slind, Mike Whalen

Proceedings of the 2014 ACM SIGAda annual conference on High integrity language technology, 2014

2013

A Step-Indexing Approach to Partial Functions

David A. Greve, Konrad Slind

Proceedings of the Proceedings International Workshop on the ACL2 Theorem Prover and its Applications, 2013

2012

The Guardol Language and Verification System.

David S. Hardin, Konrad Slind, Michael W. Whalen, Tuan-Hung Pham

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2012

A DSL for cross-domain security.

David S. Hardin, Konrad Slind, Michael W. Whalen, Tuan-Hung Pham

Proceedings of the 2012 ACM Conference on High Integrity Language Technology, 2012

Decompilation into logic - Improved.

Magnus O. Myreen, Michael J. C. Gordon, Konrad Slind

Proceedings of the Formal Methods in Computer-Aided Design, 2012

2010

Compiling Higher Order Logic by Proof.

Konrad Slind, Guodong Li, Scott Owens

Proceedings of the Design and Verification of Microprocessor Systems for High-Assurance Applications., 2010

2009

Computer Assisted Reasoning.

Richard J. Boulton, Joe Hurd, Konrad Slind

J. Autom. Reason., 2009

Extensible Proof-Producing Compilation.

Magnus O. Myreen, Konrad Slind, Michael J. C. Gordon

Proceedings of the Compiler Construction, 18th International Conference, 2009

2008

Adapting functional programs to higher order logic.

Scott Owens, Konrad Slind

High. Order Symb. Comput., 2008

A Brief Overview of HOL4.

Konrad Slind, Michael Norrish

Proceedings of the Theorem Proving in Higher Order Logics, 21st International Conference, 2008

Trusted Source Translation of a Total Function Language.

Guodong Li, Konrad Slind

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2008

Machine-Code Verification for Multiple Architectures - An Application of Decompilation into Logic.

Magnus O. Myreen, Michael J. C. Gordon, Konrad Slind

Proceedings of the Formal Methods in Computer-Aided Design, 2008

2007

Proof producing synthesis of arithmetic and cryptographic hardware.

Konrad Slind, Scott Owens, Juliano Iyoda, Mike Gordon

Formal Aspects Comput., 2007

Proof Pearl: Wellfounded Induction on the Ordinals Up to <i>epsilon</i> ₀.

Matt Kaufmann, Konrad Slind

Proceedings of the Theorem Proving in Higher Order Logics, 20th International Conference, 2007

Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic.

Guodong Li, Scott Owens, Konrad Slind

Proceedings of the Programming Languages and Systems, 2007

Compilation as Rewriting in Higher Order Logic.

Guodong Li, Konrad Slind

Proceedings of the Automated Deduction, 2007

2006

HOL.

John Harrison, Konrad Slind, Rob Arthan

Proceedings of the Seventeen Provers of the World, Foreword by Dana S. Scott, 2006

2005

Live sequence charts applied to hardware requirements specification and verification.

Annette Bunker, Ganesh Gopalakrishnan, Konrad Slind

Int. J. Softw. Tools Technol. Transf., 2005

Automatic Formal Synthesis of Hardware from Higher Order Logic.

Mike Gordon, Juliano Iyoda, Scott Owens, Konrad Slind

Proceedings of the 5th International Workshop on Automated Verification of Critical Systems, 2005

Proof Pearl: Using Combinators to Manipulate let-Expressions in Proof.

Michael Norrish, Konrad Slind

Proceedings of the Theorem Proving in Higher Order Logics, 18th International Conference, 2005

Functional Correctness Proofs of Encryption Algorithms.

Jianjun Duan, Joe Hurd, Guodong Li, Scott Owens, Konrad Slind, Junxing Zhang

Proceedings of the Logic for Programming, 2005

Counterexample Guided Invariant Discovery for Parameterized Cache Coherence Verification.

Sudhindra Pandav, Konrad Slind, Ganesh Gopalakrishnan

Proceedings of the Correct Hardware Design and Verification Methods, 2005

2004

Nemos: A Framework for Axiomatic and Executable Specifications of Memory Consistency Models.

Yue Yang, Ganesh Gopalakrishnan, Gary Lindstrom, Konrad Slind

Proceedings of the 18th International Parallel and Distributed Processing Symposium (IPDPS 2004), 2004

2003

The PROSPER toolkit.

Louise A. Dennis, Graham Collins, Michael Norrish, Richard J. Boulton, Konrad Slind, Thomas F. Melham

Int. J. Softw. Tools Technol. Transf., 2003

Applications of Polytypism in Theorem Proving.

Konrad Slind, Joe Hurd

Proceedings of the Theorem Proving in Higher Order Logics, 16th International Conference, 2003

Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SAT.

Yue Yang, Ganesh Gopalakrishnan, Gary Lindstrom, Konrad Slind

Proceedings of the Correct Hardware Design and Verification Methods, 2003

Executing the Formal Semantics of the Accellera Property Specification Language by Mechanised Theorem Proving.

Michael J. C. Gordon, Joe Hurd, Konrad Slind

Proceedings of the Correct Hardware Design and Verification Methods, 2003

2002

A Thread of HOL Development.

Michael Norrish, Konrad Slind

Comput. J., 2002

2000

Another Look at Nested Recursion.

Konrad Slind

Proceedings of the Theorem Proving in Higher Order Logics, 13th International Conference, 2000

The PROSPER Toolkit.

Louise A. Dennis, Graham Collins, Michael Norrish, Richard J. Boulton, Konrad Slind, Graham Robinson, Michael J. C. Gordon, Thomas F. Melham

Proceedings of the Tools and Algorithms for Construction and Analysis of Systems, 2000

Automatic Derivation and Application of Induction Schemes for Mutually Recursive Functions.

Richard J. Boulton, Konrad Slind

Proceedings of the Computational Logic, 2000

Wellfounded Schematic Definitions.

Konrad Slind

Proceedings of the Automated Deduction, 2000

1999

Reasoning about terminating functional programs.

Konrad Slind

PhD thesis, 1999

1998

An Interface between Clam and HOL.

Richard J. Boulton, Konrad Slind, Alan Bundy, Michael J. C. Gordon

Proceedings of the Theorem Proving in Higher Order Logics, 11th International Conference, 1998

Iterative Dialogue and Automated Proofs.

Konrad Slind, Richard J. Boulton

Proceedings of the Frontiers of Combining Systems, Second International Workshop, 1998

System Description: An Interface Between CL^AM and HOL.

Konrad Slind, Michael J. C. Gordon, Richard J. Boulton, Alan Bundy

Proceedings of the Automated Deduction, 1998

1997

Treating Partiality in a Logic of Total Functions.

Olaf Müller, Konrad Slind

Comput. J., 1997

Derivation and Use of Induction Schemes in Higher-Order Logic.

Konrad Slind

Proceedings of the Theorem Proving in Higher Order Logics, 10th International Conference, 1997

1996

Function Definition in Higher-Order Logic.

Konrad Slind

Proceedings of the Theorem Proving in Higher Order Logics, 9th International Conference, 1996

1994

I/Q Automata in Isabelle/HOL.

Tobias Nipkow, Konrad Slind

Proceedings of the Types for Proofs and Programs, 1994

A Parameterized Proof Manager.

Konrad Slind

Proceedings of the Higher Order Logic Theorem Proving and Its Applications, 1994

1993

AC Unification in HOL90.

Konrad Slind

Proceedings of the Higher Order Logic Theorem Proving and its Applications, 1993

1992

Adding New Rules to an LCF-style Logic Implementation.

Konrad Slind

Proceedings of the Higher Order Logic Theorem Proving and its Applications, 1992

1987

Monitoring Distributed Systems.

Jeffrey Joyce, Greg Lomow, Konrad Slind, Brian W. Unger

ACM Trans. Comput. Syst., 1987