Search results for "hoare-logics"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
76	Maria João Frade, Ando Saabas, Tarmo Uustalu	Foundational certification of data-flow analyses.	TASE	2007	DBLP DOI BibTeX RDF	data-flow analyses, certification of analyses and optimizations, applied vs. foundational, type systems, program optimizations, Hoare logics, natural semantics
65	Ursula Martin, Erik Arne Mathiesen, Paulo Oliva	Hoare Logic in the Abstract.	CSL	2006	DBLP DOI BibTeX RDF
53	Mark Moriconi, Richard L. Schwartz	Automatic Construction of Verification Condition Generators From Hoare Logics.	ICALP	1981	DBLP DOI BibTeX RDF
51	Frank S. de Boer, Cees Pierik	How to Cook a Complete Hoare Logic for Your Pet OO Language.	FMCO	2003	DBLP DOI BibTeX RDF
43	Tobias Nipkow	Hoare Logics for Recursive Procedures and Unbounded Nondeterminism.	CSL	2002	DBLP DOI BibTeX RDF
35	Ando Saabas, Tarmo Uustalu	Proof optimization for partial redundancy elimination.	PEPM	2008	DBLP DOI BibTeX RDF	program proof transformation, soundness and improvement of dataflow analyses and optimizations, type systems, proof-carrying code, partial redundancy elimination
35	David von Oheimb, Tobias Nipkow	Hoare Logic for NanoJava: Auxiliary Variables, Side Effects, and Virtual Methods Revisited.	FME	2002	DBLP DOI BibTeX RDF	Java, Hoare logic, side effects, dynamic binding, Isabelle/HOL, auxiliary variables
31	Tjark Weber	Towards Mechanized Program Verification with Separation Logic.	CSL	2004	DBLP DOI BibTeX RDF	Separation Logic, Interactive Theorem Proving, Formal Program Verification
29	Judicaël Courant, Marion Daubignard, Cristian Ene, Pascal Lafourcade 0001, Yassine Lakhnech	Towards automated proofs for asymmetric encryption schemes in the random oracle model.	CCS	2008	DBLP DOI BibTeX RDF	asymmetric encryption, automated proofs, provable security, hoare logics, random oracle model
29	Martin Berger 0001, Kohei Honda 0001, Nobuko Yoshida	A logical analysis of aliasing in imperative higher-order functions.	ICFP	2005	DBLP DOI BibTeX RDF	functional programming, typing, aliasing, hoare-logics, ?-calculus, pointers, modalities
27	Ramana Nagasamudram, Anindya Banerjee 0001, David A. Naumann	Alignment complete relational Hoare logics for some and all.	CoRR	2023	DBLP DOI BibTeX RDF
27	Ramana Nagasamudram, David A. Naumann	Alignment Completeness for Relational Hoare Logics.	CoRR	2021	DBLP BibTeX RDF
27	Ramana Nagasamudram, David A. Naumann	Alignment Completeness for Relational Hoare Logics.	LICS	2021	DBLP DOI BibTeX RDF
27	Simon Foster 0001, Jonathan Julián Huerta y Munive, Georg Struth	Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL.	RAMiCS	2020	DBLP DOI BibTeX RDF
27	Simon Foster 0001, Jonathan Julián Huerta y Munive, Georg Struth	Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL.	CoRR	2019	DBLP BibTeX RDF
27	Maximilian P. L. Haslbeck, Tobias Nipkow	Hoare Logics for Time Bounds.	Arch. Formal Proofs	2018	DBLP BibTeX RDF
27	Maximilian P. L. Haslbeck, Tobias Nipkow	Hoare Logics for Time Bounds - A Study in Meta Theory.	TACAS (1)	2018	DBLP DOI BibTeX RDF
27	Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin	Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs.	MPC	2012	DBLP DOI BibTeX RDF
27	Rob Arthan, Ursula Martin, Erik Arne Mathiesen, Paulo Oliva	A general framework for sound and complete Floyd-Hoare logics.	ACM Trans. Comput. Log.	2009	DBLP DOI BibTeX RDF
27	Rob Arthan, Ursula Martin, Erik Arne Mathiesen, Paulo Oliva	A General Framework for Sound and Complete Floyd-Hoare Logics	CoRR	2008	DBLP BibTeX RDF
27	Norbert Schirmer	A Sequential Imperative Programming Language Syntax, Semantics, Hoare Logics and Verification Environment.	Arch. Formal Proofs	2008	DBLP BibTeX RDF
27	Tobias Nipkow	Abstract Hoare Logics.	Arch. Formal Proofs	2006	DBLP BibTeX RDF
27	Matthew J. Parkinson, Richard Bornat, Cristiano Calcagno	Variables as Resource in Hoare Logics.	LICS	2006	DBLP DOI BibTeX RDF
27	Bernhard Reus, Thomas Streicher	About Hoare Logics for Higher-Order Store.	ICALP	2005	DBLP DOI BibTeX RDF
27	Antoni Diller	Z and Hoare Logics.	Z User Workshop	1991	DBLP BibTeX RDF
27	Michal Grabowski, Hardi Hungar	On the Existence of Effective Hoare Logics	LICS	1988	DBLP DOI BibTeX RDF
27	Michal Grabowski	On Relative Completeness of Hoare Logics	Inf. Control.	1985	DBLP DOI BibTeX RDF
27	Edmund M. Clarke, Steven M. German, Joseph Y. Halpern	Effective Axiomatizations of Hoare Logics	J. ACM	1983	DBLP DOI BibTeX RDF
27	Edmund M. Clarke, Steven M. German, Joseph Y. Halpern	On Effective Axiomatizations of Hoare Logics.	POPL	1982	DBLP DOI BibTeX RDF
27	Richard J. Lipton	A Necessary and Sufficient Condition for the Existence of Hoare Logics	FOCS	1977	DBLP DOI BibTeX RDF
15	Asma Louhichi, Olfa Mraihi, Lamia Labed Jilani, Khaled Bsaïes, Ali Mili 0001	Relational Methods in the Analysis of While Loops: Observations of Versatility.	RelMiCS	2009	DBLP DOI BibTeX RDF	Function extraction, loop functions, invariant assertions, invariant relations, invariant functions, computing loop behavior, refinement calculus, relational calculus
15	Bernd Fischer 0002, Ando Saabas, Tarmo Uustalu	Program Repair as Sound Optimization of Broken Programs.	TASE	2009	DBLP DOI BibTeX RDF
15	Veronika Ortner, Norbert Schirmer	Verification of BDD Normalization.	TPHOLs	2005	DBLP DOI BibTeX RDF
15	Phan Minh Dung, Phan Minh Thang	Stepwise development of security protocols: a speech act-oriented approach.	FMSE	2004	DBLP DOI BibTeX RDF	security protocols, cryptographic protocols
15	Cees Pierik, Frank S. de Boer	Modularity and the Rule of Adaptation.	AMAST	2004	DBLP DOI BibTeX RDF
15	Frank S. de Boer	Reasoning about Asynchronous Communication in Dynamically Evolving Object Structures.	CONCUR	1998	DBLP DOI BibTeX RDF
15	Job Zwiers, Ulrich Hannemann, Yassine Lakhnech, Willem P. de Roever, Frank A. Stomp	Modular Completeness: Integrating the Reuse of Specified Software in Top-down Program Development.	FME	1996	DBLP DOI BibTeX RDF