Konrad Slind - RankMe

55 papers A 9B 6Journal 13Unranked 23

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