Search results for "Higher-order-logic"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
5	Giampaolo Bella, Pietro Liò	Formal Analysis of the Genetic Toggle.	CMSB	2009	DBLP DOI BibTeX RDF
5	Jesús Aransay, Clemens Ballarin, Julio Rubio 0001	A Mechanized Proof of the Basic Perturbation Lemma.	J. Autom. Reason.	2008	DBLP DOI BibTeX RDF	Homological algebra, Basic perturbation lemma, Isabelle
5	Konrad Slind, Michael Norrish	A Brief Overview of HOL4.	TPHOLs	2008	DBLP DOI BibTeX RDF
5	Achim D. Brucker, Lukas Brügger, Burkhart Wolff	Model-Based Firewall Conformance Testing.	TestCom/FATES	2008	DBLP DOI BibTeX RDF	Model-based Testing, Firewall, Conformance Testing, Security Testing
5	Youngsik Kim, Nazanin Mansouri	Automated formal verification of scheduling with speculative code motions.	ACM Great Lakes Symposium on VLSI	2008	DBLP DOI BibTeX RDF	formal verification, high level synthesis, automated theorem-proving, speculation
5	Chunqing Chen, Jin Song Dong, Jun Sun 0001	A verification system for timed interval calculus.	ICSE	2008	DBLP DOI BibTeX RDF	real-time systems, theorem proving, specification language, pvs
5	Amine Chaieb	Parametric Linear Arithmetic over Ordered Fields in Isabelle/HOL.	AISC/MKM/Calculemus	2008	DBLP DOI BibTeX RDF
5	Paul Curzon, Rimvydas Ruksenas, Ann Blandford	An approach to formal verification of human-computer interaction.	Formal Aspects Comput.	2007	DBLP DOI BibTeX RDF	Formal cognitive architecture, Formal verification, Theorem proving, Interactive systems, Human error
5	Steven Obua	Proof Pearl: Looping Around the Orbit.	TPHOLs	2007	DBLP DOI BibTeX RDF
5	Joe Hurd	Proof Pearl: The Termination Analysis of Terminator.	TPHOLs	2007	DBLP DOI BibTeX RDF
5	Osman Hasan, Sofiène Tahar	Formalization of Continuous Probability Distributions.	CADE	2007	DBLP DOI BibTeX RDF
5	Carsten Schürmann, Mark-Oliver Stehr	An Executable Formalization of the HOL/Nuprl Connection in the Metalogical Framework Twelf.	LPAR	2006	DBLP DOI BibTeX RDF
5	Philippe Audebaud, Christine Paulin-Mohring	Proofs of Randomized Algorithms in Coq.	MPC	2006	DBLP DOI BibTeX RDF
5	Steven Obua	Partizan Games in Isabelle/HOLZF.	ICTAC	2006	DBLP DOI BibTeX RDF
5	Adam Biltcliffe, Michael Dales, Sam Jansen, Tom Ridge, Peter Sewell	Rigorous Protocol Design in Practice: An Optical Packet-Switch MAC in HOL.	ICNP	2006	DBLP DOI BibTeX RDF
5	Abu Nasser Mohammed Abdullah, Behzad Akbarpour, Sofiène Tahar	Formal Analysis and Verification of an OFDM Modem Design using HOL.	FMCAD	2006	DBLP DOI BibTeX RDF
5	Philip Derrin, Kevin Elphinstone, Gerwin Klein, David A. Cock, Manuel M. T. Chakravarty	Running the manual: an approach to high-assurance microkernel development.	Haskell	2006	DBLP DOI BibTeX RDF	formalisation, verification, operating systems, rapid prototyping, Haskell, monads, executable specification, Isabelle/HOL
5	John M. Rushby	Tutorial: Automated Formal Methods with PVS, SAL, and Yices.	SEFM	2006	DBLP DOI BibTeX RDF
5	Behzad Akbarpour, Sofiène Tahar, Abdelkader Dekdouk	Formalization of Fixed-Point Arithmetic in HOL.	Formal Methods Syst. Des.	2005	DBLP DOI BibTeX RDF	theorem-proving, floating-point arithmetic, fixed-point arithmetic, HOL
5	Claire J. Thie, Christophe G. Giraud-Carrier	Learning Concept Descriptions with Typed Evolutionary Programming.	IEEE Trans. Knowl. Data Eng.	2005	DBLP DOI BibTeX RDF	typed evolutionary programming, Concept learning
5	Cristina Cerschi Seceleanu	Formal Development of Real-Time Priority-Based Schedulers.	ECBS	2005	DBLP DOI BibTeX RDF
5	Amine Chaieb, Tobias Nipkow	Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic.	LPAR	2005	DBLP DOI BibTeX RDF
5	Jianjun Duan, Joe Hurd, Guodong Li, Scott Owens, Konrad Slind, Junxing Zhang	Functional Correctness Proofs of Encryption Algorithms.	LPAR	2005	DBLP DOI BibTeX RDF
5	Andrew M. Pitts	Alpha-Structural Recursion and Induction.	TPHOLs	2005	DBLP DOI BibTeX RDF
5	Nicolas Sklavos 0001, Nick A. Moldovyan, Vladimir Gorodetsky, Odysseas G. Koufopavlou	Computer Network Security: Report from MMM-ACNS.	IEEE Secur. Priv.	2004	DBLP DOI BibTeX RDF	WMMM, ACNS, architectures, mathematical models, conference
5	Lutz Schröder, Till Mossakowski, Christoph Lüth	Type Class Polymorphism in an Institutional Framework.	WADT	2004	DBLP DOI BibTeX RDF
5	Arnd Poetzsch-Heffter, Nicole Rauch	Application and Formal Specification of Sorted Term-Position Algebras.	WADT	2004	DBLP DOI BibTeX RDF
5	John O'Leary	Formal verification in Intel CPU design.	MEMOCODE	2004	DBLP DOI BibTeX RDF
5	Stefan Richter 0001	Formalizing Integration Theory with an Application to Probabilistic Algorithms.	TPHOLs	2004	DBLP DOI BibTeX RDF
5	Lucas Dixon, Jacques D. Fleuriot	Higher Order Rippling in IsaPlanner.	TPHOLs	2004	DBLP DOI BibTeX RDF
5	Morten P. Lindegaard, Anne E. Haxthausen	Proof Support for RAISE by a Reuse Approach Based on Institutions.	AMAST	2004	DBLP DOI BibTeX RDF	proof support, Institutions, algebraic semantics, HOL, RSL
5	K. Gopinath, Anil K. Pugalia, K. V. M. Naidu	Formal Proof of Impossibility of Reliability in Crashing Protocols.	IWDC	2004	DBLP DOI BibTeX RDF
5	Behzad Akbarpour, Sofiène Tahar	Modeling System C Fixed-Point Arithmetic in HOL.	ICFEM	2003	DBLP DOI BibTeX RDF
5	Laura I. Meikle, Jacques D. Fleuriot	Formalizing Hilbert's Grundlagen in Isabelle/Isar.	TPHOLs	2003	DBLP DOI BibTeX RDF
5	Konrad Slind, Joe Hurd	Applications of Polytypism in Theorem Proving.	TPHOLs	2003	DBLP DOI BibTeX RDF
5	Leonor Prensa Nieto	The Rely-Guarantee Method in Isabelle/HOL.	ESOP	2003	DBLP DOI BibTeX RDF
5	Michael J. C. Gordon, Joe Hurd, Konrad Slind	Executing the Formal Semantics of the Accellera Property Specification Language by Mechanised Theorem Proving.	CHARME	2003	DBLP DOI BibTeX RDF
5	Stefan Edelkamp, Peter Leven	Directed Automated Theorem Proving.	LPAR	2002	DBLP DOI BibTeX RDF
5	Achim D. Brucker, Burkhart Wolff	HOL-OCL: Experiences, Consequences and Design Choices.	UML	2002	DBLP DOI BibTeX RDF	refinement, OCL, formal semantics, constraint languages
5	David von Oheimb	Interacting State Machines: A Stateful Approach to Proving Security.	FASec	2002	DBLP DOI BibTeX RDF
5	Jean-Paul Bodeveix, Mamoun Filali	Type Synthesis in B and the Translation of B to PVS.	ZB	2002	DBLP DOI BibTeX RDF	semantics, type theory, PVS, logical frameworks, B
5	Behzad Akbarpour, Abdelkader Dekdouk, Sofiène Tahar	Formalization of Cadence SPW Fixed-Point Arithmetic in HOL.	IFM	2002	DBLP DOI BibTeX RDF	SPW, Theorem-Proving, Signal Processing, Floating-point, Fixed-point, HOL
5	Marieke Huisman, Bart Jacobs 0001, Joachim van den Berg	A case study in class library verification: Java's vector class.	Int. J. Softw. Tools Technol. Transf.	2001	DBLP DOI BibTeX RDF	Java, Specification, Program verification, Invariant
5	Andrew W. Appel, David A. McAllester	An indexed model of recursive types for foundational proof-carrying code.	ACM Trans. Program. Lang. Syst.	2001	DBLP DOI BibTeX RDF
5	Viktor K. Sabelfeld, Christian Blumenröhr, Kai Kapp	Semantics and Transformations in Formal Synthesis at System Level.	Ershov Memorial Conference	2001	DBLP DOI BibTeX RDF
5	Paul Curzon, Ann Blandford	Detecting Multiple Classes of User Errors.	EHCI	2001	DBLP DOI BibTeX RDF
5	Steffen Helke, Thomas Santen	Mechanized Analysis of Behavioral Conformance in the Eiffel Base Libraries.	FME	2001	DBLP DOI BibTeX RDF
5	Joachim van den Berg, Bart Jacobs 0001	The LOOP Compiler for Java and JML.	TACAS	2001	DBLP DOI BibTeX RDF
5	Lawrence C. Paulson	Mechanizing UNITY in Isabelle.	ACM Trans. Comput. Log.	2000	DBLP DOI BibTeX RDF	concurrency, UNITY, Isabelle, compositional reasoning
5	Carl A. Gunter, Elsa L. Gunter, Michael Jackson 0001, Pamela Zave	A Reference Model for Requirements and Specifications-Extended Abstract.	ICRE	2000	DBLP DOI BibTeX RDF	formal methods, specifications, refinement, requirements, software engineering methodology
5	Konrad Slind	Another Look at Nested Recursion.	TPHOLs	2000	DBLP DOI BibTeX RDF
5	Peter B. Andrews, Chad E. Brown	Tutorial: Using TPS for Higher-Order Theorem Proving and ETPS for Teaching Logic.	CADE	2000	DBLP DOI BibTeX RDF
5	Peter B. Andrews, Matthew Bishop, Chad E. Brown	System Description: TPS: A Theorem Proving System for Type Theory.	CADE	2000	DBLP DOI BibTeX RDF
5	Mark D. Aagaard, Robert B. Jones, Thomas F. Melham, John W. O'Leary, Carl-Johan H. Seger	A Methodology for Large-Scale Hardware Verification.	FMCAD	2000	DBLP DOI BibTeX RDF
5	Lawrence C. Paulson	Inductive Analysis of the Internet Protocol TLS.	ACM Trans. Inf. Syst. Secur.	1999	DBLP DOI BibTeX RDF	inductive method, proof tools, authentication, TLS, Isabelle
5	Don Syme	Three Tactic Theorem Proving.	TPHOLs	1999	DBLP DOI BibTeX RDF
5	Nazanin Mansouri, Ranga Vemuri	Accounting for Various Register Allocation Schemes During Post-Synthesis Verification of RTL Designs.	DATE	1999	DBLP DOI BibTeX RDF
5	John Herbert, Bruno Dutertre, Robert A. Riemenschneider, Victoria Stavridou	A Formalization of Software Architecture.	World Congress on Formal Methods	1999	DBLP DOI BibTeX RDF
5	David Spelt, Susan Even	A Theorem Prover-Based Analysis Tool for Object-Oriented Databases.	TACAS	1999	DBLP DOI BibTeX RDF
5	Abhijit Ghosh, Ranga Vemuri	Formal Verification of Synthesized Analog Designs.	ICCD	1999	DBLP DOI BibTeX RDF
5	Peter Frey, Radharamanan Radhakrishnan, Philip A. Wilsey, Perry Alexander, Harold W. Carter	An Extensible Formal Framework for the Specification and Verification of an Optimistic Simulation Protocol.	HICSS	1999	DBLP DOI BibTeX RDF	Software Engineering, Theorem Proving, Parallel Discrete Event Simulation, PVS, Formal specification and verification
5	Bart Jacobs 0001, Joachim van den Berg, Marieke Huisman, Martijn van Berkum	Reasoning about Java Classes (Preliminary Report).	OOPSLA	1998	DBLP DOI BibTeX RDF	Java
5	Naren Narasimhan, Ranga Vemuri	On the Effectiveness of Theorem Proving Guided Discovery of Formal Assertions for a Register Allocator in a High-Level Synthesis System.	TPHOLs	1998	DBLP DOI BibTeX RDF
5	Mark E. Woodcock	The wHOLe System.	FM-Trends	1998	DBLP DOI BibTeX RDF
5	Christian Blumenröhr, Dirk Eisenbiegler	Performing High-Level Synthesis via Program Transformations within a Theorem Prover.	EUROMICRO	1998	DBLP DOI BibTeX RDF
5	Sofiène Tahar, Paul Curzon, Jianping Lu	Three Approaches to Hardware Verification: HOL, MDG and VIS Compared.	FMCAD	1998	DBLP DOI BibTeX RDF
5	Annette Bunker, Trent N. Larson, Michael D. Jones, Phillip J. Windley	Alexandria: A Tool for Hierarchical Verification.	FMCAD	1998	DBLP DOI BibTeX RDF
5	Thomas Lock, Michael Mendler, Matthias Mutz	Combined Formal Post- and Presynthesis Verification in High Level Synthesis.	FMCAD	1998	DBLP DOI BibTeX RDF
5	Marco Devillers, W. O. David Griffioen, Olaf Müller	Possibly Infinite Sequences in Theorem Provers: A Comparative Study.	TPHOLs	1997	DBLP DOI BibTeX RDF
5	Haykal Tej, Burkhart Wolff	A Corrected Failure Divergence Model for CSP in Isabelle/HOL.	FME	1997	DBLP DOI BibTeX RDF
5	David W. J. Stringer-Calvert, Susan Stepney, Ian Wand	Using PVS to Prove a Z Refinement: A Case Study.	FME	1997	DBLP DOI BibTeX RDF
5	Tobias Nipkow	More Church-Rosser Proofs (in Isabelle/HOL).	CADE	1996	DBLP DOI BibTeX RDF
5	Peter V. Homeier, David F. Martin	Mechanical Verification of Mutually Recursive Procedures.	CADE	1996	DBLP DOI BibTeX RDF
5	Shiu-Kai Chin, John Faust, Joseph Giordano	Formal Methods Applied to Secure Network Engineering.	ICECCS	1996	DBLP DOI BibTeX RDF
5	Natarajan Shankar	Verification of Real-Time Systems Using PVS.	CAV	1993	DBLP DOI BibTeX RDF
5	Nancy A. Day	An example of linking formal methods with case tools: a model checker for statecharts.	CASCON	1993	DBLP BibTeX RDF
5	Keehang Kwon, Gopalan Nadathur, Debra Sue Wilson	Implementing a Notion of Modules in the Logic Programming Language Lambda-Prolog.	ELP	1992	DBLP DOI BibTeX RDF
5	Frank Pfenning, Dan Nesmith	Presenting Intuitive Deductions via Symmetric Simplification.	CADE	1990	DBLP DOI BibTeX RDF
5	Shiu-Kai Chin	Combining Engineering Vigor with Mathematical Rigor.	Hardware Specification, Verification and Synthesis	1989	DBLP DOI BibTeX RDF
5	Aurelio Carboni, Peter J. Freyd, Andre Scedrov	A Categorical Approach to Realizability and Polymorphic Types.	MFPS	1987	DBLP DOI BibTeX RDF
5	Daniel Leivant	Structural Semantics for Polymorphic Data Types.	POPL	1983	DBLP DOI BibTeX RDF