Konrad Slind

Publication Activity (10 Years)

Years Active: 1987-2023
Publications (10 Years): 8

Top Venues

ACL2

HILT

ITP

CoRR

Technical University Munich, Germany (PHD)

Education History

Technical University Munich, Germany

PHD

Publications

Eric Mercer, Konrad Slind, Isaac Amundson, Darren D. Cofer, Junaid Babar, David S. Hardin
Synthesizing verified components for cyber assured systems engineering. Softw. Syst. Model. 22 (5) (2023)
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
Model-driven development for the seL4 microkernel using the HAMR framework. J. Syst. Archit. 134 (2023)
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
Cyberassured Systems Engineering at Scale. IEEE Secur. Priv. 20 (3) (2022)
Konrad Slind
Specifying Message Formats with Contiguity Types. ITP (2021)
Eric Mercer, Konrad Slind, Isaac Amundson, Darren D. Cofer, Junaid Babar, David S. Hardin
Synthesizing Verified Components for Cyber Assured Systems Engineering. MoDELS (2021)
David S. Hardin, Konrad Slind
Using ACL2 in the Design of Efficient, Verifiable Data Structures for High-Assurance Systems. ACL2 (2018)
Lucas G. Wagner, Alain Mebsout, Cesare Tinelli, Darren D. Cofer, Konrad Slind
Qualification of a Model Checker for Avionics Software Verification. NFM (2017)
David S. Hardin, Konrad Slind, Mark Bortz, James Potts, Scott Owens
A High-Assurance, High-Performance Hardware-Based Cross-Domain System. SAFECOMP (2016)
Darren D. Cofer, Gerwin Klein, Konrad Slind, Virginie Wiels
Qualification of Formal Methods Tools (Dagstuhl Seminar 15182). Dagstuhl Reports 5 (4) (2015)
Andrew Gacek, John Backes, Darren D. Cofer, Konrad Slind, Mike Whalen
Resolute: an assurance case language for architecture models. HILT (2014)
Andrew Gacek, John Backes, Darren D. Cofer, Konrad Slind, Mike Whalen
Resolute: An Assurance Case Language for Architecture Models. CoRR (2014)
David A. Greve, Konrad Slind
A Step-Indexing Approach to Partial Functions ACL2 (2013)
David S. Hardin, Konrad Slind, Michael W. Whalen, Tuan-Hung Pham
A DSL for cross-domain security. HILT (2012)
David S. Hardin, Konrad Slind, Michael W. Whalen, Tuan-Hung Pham
The Guardol Language and Verification System. TACAS (2012)
Magnus O. Myreen, Michael J. C. Gordon, Konrad Slind
Decompilation into logic - Improved. FMCAD (2012)
Richard J. Boulton, Joe Hurd, Konrad Slind
Computer Assisted Reasoning. J. Autom. Reason. 43 (3) (2009)
Magnus O. Myreen, Konrad Slind, Michael J. C. Gordon
Extensible Proof-Producing Compilation. CC (2009)
Magnus O. Myreen, Michael J. C. Gordon, Konrad Slind
Machine-Code Verification for Multiple Architectures - An Application of Decompilation into Logic. FMCAD (2008)
Konrad Slind, Michael Norrish
A Brief Overview of HOL4. TPHOLs (2008)
Guodong Li, Konrad Slind
Trusted Source Translation of a Total Function Language. TACAS (2008)
Scott Owens, Konrad Slind
Adapting functional programs to higher order logic. High. Order Symb. Comput. 21 (4) (2008)
Matt Kaufmann, Konrad Slind
. TPHOLs (2007)
Konrad Slind, Scott Owens, Juliano Iyoda, Mike Gordon
Proof producing synthesis of arithmetic and cryptographic hardware. Formal Aspects Comput. 19 (3) (2007)
Guodong Li, Konrad Slind
Compilation as Rewriting in Higher Order Logic. CADE (2007)
Guodong Li, Scott Owens, Konrad Slind
Structure of a Proof-Producing Compiler for a Subset of Higher Order Logic. ESOP (2007)
Mike Gordon, Juliano Iyoda, Scott Owens, Konrad Slind
Automatic Formal Synthesis of Hardware from Higher Order Logic. Electron. Notes Theor. Comput. Sci. 145 (2006)
Sudhindra Pandav, Konrad Slind, Ganesh Gopalakrishnan
Counterexample Guided Invariant Discovery for Parameterized Cache Coherence Verification. CHARME (2005)
Jianjun Duan, Joe Hurd, Guodong Li, Scott Owens, Konrad Slind, Junxing Zhang
Functional Correctness Proofs of Encryption Algorithms. LPAR (2005)
Annette Bunker, Ganesh Gopalakrishnan, Konrad Slind
Live sequence charts applied to hardware requirements specification and verification. Int. J. Softw. Tools Technol. Transf. 7 (4) (2005)
Michael Norrish, Konrad Slind
Proof Pearl: Using Combinators to Manipulate let-Expressions in Proof. TPHOLs (2005)
Yue Yang, Ganesh Gopalakrishnan, Gary Lindstrom, Konrad Slind
Nemos: A Framework for Axiomatic and Executable Specifications of Memory Consistency Models. IPDPS (2004)
Yue Yang, Ganesh Gopalakrishnan, Gary Lindstrom, Konrad Slind
Analyzing the Intel Itanium Memory Ordering Rules Using Logic Programming and SAT. CHARME (2003)
Michael J. C. Gordon, Joe Hurd, Konrad Slind
Executing the Formal Semantics of the Accellera Property Specification Language by Mechanised Theorem Proving. CHARME (2003)
Konrad Slind, Joe Hurd
Applications of Polytypism in Theorem Proving. TPHOLs (2003)
Louise A. Dennis, Graham Collins, Michael Norrish, Richard J. Boulton, Konrad Slind, Thomas F. Melham
The PROSPER toolkit. Int. J. Softw. Tools Technol. Transf. 4 (2) (2003)
Michael Norrish, Konrad Slind
A Thread of HOL Development. Comput. J. 45 (1) (2002)
Louise A. Dennis, Graham Collins, Michael Norrish, Richard J. Boulton, Konrad Slind, Graham Robinson, Michael J. C. Gordon, Thomas F. Melham
The PROSPER Toolkit. TACAS (2000)
Konrad Slind
Another Look at Nested Recursion. TPHOLs (2000)
Konrad Slind
Wellfounded Schematic Definitions. CADE (2000)
Richard J. Boulton, Konrad Slind
Automatic Derivation and Application of Induction Schemes for Mutually Recursive Functions. Computational Logic (2000)
Konrad Slind, Michael J. C. Gordon, Richard J. Boulton, Alan Bundy
M and HOL. CADE (1998)
Richard J. Boulton, Konrad Slind, Alan Bundy, Michael J. C. Gordon
An Interface between Clam and HOL. TPHOLs (1998)
Konrad Slind, Richard J. Boulton
Iterative Dialogue and Automated Proofs. FroCoS (1998)
Konrad Slind
Derivation and Use of Induction Schemes in Higher-Order Logic. TPHOLs (1997)
Olaf Müller, Konrad Slind
Treating Partiality in a Logic of Total Functions. Comput. J. 40 (10) (1997)
Konrad Slind
Function Definition in Higher-Order Logic. TPHOLs (1996)
Tobias Nipkow, Konrad Slind
I/Q Automata in Isabelle/HOL. TYPES (1994)
Konrad Slind
A Parameterized Proof Manager. TPHOLs (1994)
Konrad Slind
AC Unification in HOL90. HUG (1993)
Konrad Slind
Adding New Rules to an LCF-style Logic Implementation. TPHOLs (1992)
Jeffrey Joyce, Greg Lomow, Konrad Slind, Brian W. Unger
Monitoring Distributed Systems. ACM Trans. Comput. Syst. 5 (2) (1987)

Konrad Slind.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Konrad Slind