Search results for "Hoare-logic"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
105	Thomas Kleymann	Hoare Logic and Auxiliary Variables.	Formal Aspects Comput.	1999	DBLP DOI BibTeX RDF	Adaptation Completeness, Most General Formula, Hoare Logic, VDM, Auxiliary variables
90	Ursula Martin, Erik Arne Mathiesen, Paulo Oliva	Hoare Logic in the Abstract.	CSL	2006	DBLP DOI BibTeX RDF
82	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
82	David von Oheimb	Hoare Logic for Mutual Recursion and Local Variables.	FSTTCS	1999	DBLP DOI BibTeX RDF	axiomaticsemantics, relative completeness, local variables, call-by-value parameters, soundness, Hoare logic, Isabelle/HOL, mutual recursion
77	Pei He, Lishan Kang, Daochang Huang	Construction of Hoare Triples under Generalized Model with Semantically Valid Genetic Operations.	ISICA	2009	DBLP DOI BibTeX RDF	finite state automaton, model checking, Genetic programming, Hoare logic
70	Dexter Kozen	On Hoare logic and Kleene algebra with tests.	ACM Trans. Comput. Log.	2000	DBLP DOI BibTeX RDF	specification, dynamic logic, Hoare logic, Kleene algebra, Kleene algebra with tests
66	Frank S. de Boer, Cees Pierik	How to Cook a Complete Hoare Logic for Your Pet OO Language.	FMCO	2003	DBLP DOI BibTeX RDF
63	Zhaozhong Ni, Zhong Shao	Certified assembly programming with embedded code pointers.	POPL	2006	DBLP DOI BibTeX RDF	embedded code pointers, hoare logic, proof-carrying code, higher-order functions
58	Dexter Kozen	On Hoare Logic and Kleene Algebra with Tests.	LICS	1999	DBLP DOI BibTeX RDF	combination of logics, verification, formal methods, universal algebra, logics of programs
58	Ernie Cohen, Dexter Kozen	A note on the complexity of propositional Hoare logic.	ACM Trans. Comput. Log.	2000	DBLP DOI BibTeX RDF	specification, Hoare logic
57	Cristiano Calcagno, Philippa Gardner, Uri Zarfaty	Context logic and tree update.	POPL	2005	DBLP DOI BibTeX RDF	tree update, contexts, hoare logic
51	Yiyun Chen, Lin Ge, Baojian Hua, Zhaopeng Li, Cheng Liu, Zhifang Wang	A pointer logic and certifying compiler.	Frontiers Comput. Sci. China	2007	DBLP DOI BibTeX RDF	pointer logic, Hoare logic, Proof-Carrying Code, software safety, certifying compiler
50	Magnus O. Myreen, Anthony C. J. Fox, Michael J. C. Gordon	Hoare Logic for ARM Machine Code.	FSEN	2007	DBLP DOI BibTeX RDF
49	Hongxu Cai, Zhong Shao, Alexander Vaynberg	Certified self-modifying code.	PLDI	2007	DBLP DOI BibTeX RDF	assembly code verification, runtime code manipulation, self-modifying code, hoare logic, modular verification
49	Aleksandar Nanevski, Greg Morrisett, Lars Birkedal	Polymorphism and separation in hoare type theory.	ICFP	2006	DBLP DOI BibTeX RDF	type theory, hoare logic, separation logic
47	Sunae Seo, Hongseok Yang, Kwangkeun Yi, Taisook Han	Goal-directed weakening of abstract interpretation results.	ACM Trans. Program. Lang. Syst.	2007	DBLP DOI BibTeX RDF	static analysis, Abstract interpretation, program verification, Hoare logic, backward analysis
47	Nick Benton	Simple relational correctness proofs for static analyses and program transformations.	POPL	2004	DBLP DOI BibTeX RDF	partial equivalence relations, security, dependency, program analysis, information flow, types, optimizing compilation, denotational semantics, Hoare logic
46	Marieke Huisman, Bart Jacobs 0001	Java Program Verification via a Hoare Logic with Abrupt Termination.	FASE	2000	DBLP DOI BibTeX RDF
46	Jan Friso Groote, Alban Ponse	Process Algebra with Guards - Combining Hoare Logic with Process Algebra (Extended Abstract).	CONCUR	1991	DBLP DOI BibTeX RDF
46	Stephen L. Bloom, Zoltán Ésik	Floyd-Hoare Logic in Iteration Theories.	J. ACM	1991	DBLP DOI BibTeX RDF	correction assertions, Hoare logic
46	Jerry den Hartog	Verifying Probabilistic Programs Using a Hoare like Logic.	ASIAN	1999	DBLP DOI BibTeX RDF
45	Lena Verscht, Benjamin Lucien Kaminski	Hoare-Like Triples and Kleene Algebras with Top and Tests: Towards a Holistic Perspective on Hoare Logic, Incorrectness Logic, and Beyond.	CoRR	2023	DBLP DOI BibTeX RDF
45	Andreas Goerdt	Hoare Logic for Lambda-Terms as Basis of Hoare Logic for Imperative Languages	LICS	1987	DBLP BibTeX RDF
45	Cees Pierik, Frank S. de Boer	A Syntax-Directed Hoare Logic for Object-Oriented Programming Concepts.	FMOODS	2003	DBLP DOI BibTeX RDF
40	Matthew J. Parkinson, Richard Bornat, Cristiano Calcagno	Variables as Resource in Hoare Logics.	LICS	2006	DBLP DOI BibTeX RDF
39	A. Udaya Shankar	An Introduction to Assertional Reasoning for Concurrent Systems.	ACM Comput. Surv.	1993	DBLP DOI BibTeX RDF	generation of preconditions, leads-to, progress properties, invariants, Hoare logic, weakest preconditions, safety properties, state transition systems, assertional reasoning
37	Hayo Thielecke	Frame rules from answer types for code pointers.	POPL	2006	DBLP DOI BibTeX RDF	code pointers, polymorphism, continuations, Hoare logic, typed assembly language
37	Yann Régis-Gianas, François Pottier	A Hoare Logic for Call-by-Value Functional Programs.	MPC	2008	DBLP DOI BibTeX RDF
37	Nadeem Abdul Hamid, Zhong Shao	Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code.	TPHOLs	2004	DBLP DOI BibTeX RDF
36	Andrew M. Gravell	Verification conditions are code.	Acta Informatica	2007	DBLP DOI BibTeX RDF
36	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
36	Sunae Seo, Hongseok Yang, Kwangkeun Yi	Automatic Construction of Hoare Proofs from Abstract Interpretation Results.	APLAS	2003	DBLP DOI BibTeX RDF
35	Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin	Formal certification of code-based cryptographic proofs.	POPL	2009	DBLP DOI BibTeX RDF	cryptographic proofs, relational hoare logic, program transformations, observational equivalence, coq proof assistant
35	Khair Eddin Sabri, Ridha Khédri, Jason Jaskolka	Verification of Information Flow in Agent-Based Systems.	MCETECH	2009	DBLP DOI BibTeX RDF	Global calculus, Information Algebra, Agent Knowledge, Information Flow, Hoare Logic
35	Jean-Christophe Filliâtre, Claude Marché	Multi-prover Verification of C Programs.	ICFEM	2004	DBLP DOI BibTeX RDF	pointer programs, formal verification and proof, Hoare logic, C programming language
35	Dexter Kozen, Jerzy Tiuryn	Substructural logic and partial correctness.	ACM Trans. Comput. Log.	2003	DBLP DOI BibTeX RDF	specification, linear logic, Dynamic logic, Hoare logic, sequent calculus, substructural logic, Kleene algebra, Kleene algebra with tests
35	Andreas Blass, Yuri Gurevich	Inadequacy of computable loop invariants.	ACM Trans. Comput. Log.	2001	DBLP DOI BibTeX RDF	postcondition uncomputable, recursive inseparability, assertion, automated reasoning, precondition, Hoare logic, automated deduction, loop invariants
35	Frank S. de Boer	A Proof System for the Language POOL.	REX Workshop	1990	DBLP DOI BibTeX RDF	partial correctness, completeness, Object, soundness, Hoare-logic, pointers, proof-system, rendezvous, object-creation
35	Alan C. Shaw	Reasoning About Time in Higher-Level Language Software.	IEEE Trans. Software Eng.	1989	DBLP DOI BibTeX RDF	higher-level language software, program elements, time-related statements, timing invariants, periodic processes, real-time systems, real-time, formal specification, synchronization, specification, lower bounds, delay, concurrent programs, synchronisation, upper bounds, assertions, deadlines, execution times, computer times, formal logic, Hoare logic, timing bounds, sequential programs
35	Chenguang Luo, Shengchao Qin, Zongyan Qiu	Verifying BPEL-like programs with Hoare logic.	Frontiers Comput. Sci. China	2008	DBLP DOI BibTeX RDF	compensation mechanism, axiomatic verification system, operational semantics, soundness, WS-BPEL
35	Chenguang Luo, Shengchao Qin, Zongyan Qiu	Verifying BPEL-Like Programs with Hoare Logic.	TASE	2008	DBLP DOI BibTeX RDF
34	Jean Yang 0001, Chris Hawblitzel	Safe to the last instruction: automated verification of a type-safe operating system.	PLDI	2010	DBLP DOI BibTeX RDF	verification, operating system, type safety, run-time system
34	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
32	Nancy A. Durgin, John C. Mitchell, Dusko Pavlovic	A Compositional Logic for Protocol Correctness.	CSFW	2001	DBLP DOI BibTeX RDF
28	Till Mossakowski, Lutz Schröder, Sergey Goncharov 0001	A Generic Complete Dynamic Logic for Reasoning About Purity and Effects.	FASE	2008	DBLP DOI BibTeX RDF
27	Thibault Dardinier	Formalization of Hyper Hoare Logic: A Logic to (Dis-)Prove Program Hyperproperties.	Arch. Formal Proofs	2023	DBLP BibTeX RDF
27	Yuan Feng 0001, Sanjiang Li	Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs.	Inf. Comput.	2023	DBLP DOI BibTeX RDF
27	Yuan Feng 0001, Sanjiang Li	Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs.	CoRR	2022	DBLP DOI BibTeX RDF
27	Jianhua Zhao, Xuandong Li	Scope Logic: An Extension to Hoare Logic for Pointers and Recursive Data Structures.	ICTAC	2013	DBLP DOI BibTeX RDF
27	Grigore Rosu, Andrei Stefanescu	From Hoare Logic to Matching Logic Reachability.	FM	2012	DBLP DOI BibTeX RDF
27	Jianhua Zhao, Xuandong Li	Scope Logic: Extending Hoare Logic for Pointer Program Verification	CoRR	2009	DBLP BibTeX RDF
27	Andreas Blass, Yuri Gurevich	The Underlying Logic of Hoare Logic.	Current Trends in Theoretical Computer Science	2001	DBLP BibTeX RDF
27	Andreas Blass, Yuri Gurevich	The Underlying Logic of Hoare Logic.	Bull. EATCS	2000	DBLP BibTeX RDF
27	Peter M. W. Knijnenburg, Frank Nordemann	Partial Hyperdoctrines: Categorical Models for Partial Function Logic and Hoare Logic.	Math. Struct. Comput. Sci.	1994	DBLP DOI BibTeX RDF
27	Norbert E. Fuchs	Hoare Logic, Executable Specifications and Logic Programs.	Struct. Program.	1992	DBLP BibTeX RDF
27	Peter M. W. Knijnenburg, Frank Nordemann	A Categorical Interpretation of Partial Function Logic and Hoare Logic.	LFCS	1992	DBLP DOI BibTeX RDF
26	Xinyu Feng 0001, Zhong Shao, Yu Guo, Yuan Dong	Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads.	J. Autom. Reason.	2009	DBLP DOI BibTeX RDF	Operating system verification, Hardware interrupts, Preemptive threads, Thread libraries, Modularity, Separation logic, Synchronization primitives
26	Xinyu Feng 0001, Zhong Shao, Yuan Dong, Yu Guo	Certifying low-level programs with hardware interrupts and preemptive threads.	PLDI	2008	DBLP DOI BibTeX RDF	certified system software, hardware interrupts, preemptive threads, concurrency, separation logic
26	Cui Zhang, Robert J. Shaw, Ronald A. Olsson, Karl N. Levitt, Myla Archer, Mark R. Heckman, Gregory D. Benson	Mechanizing a Programming Logic for the Concurrent Programming Language microSR in HOL.	HUG	1993	DBLP DOI BibTeX RDF
24	Gordon D. Plotkin, Matija Pretnar	A Logic for Algebraic Effects.	LICS	2008	DBLP DOI BibTeX RDF	call-by-push-value, computational lambda-calculus, program logics, computational effects, algebraic operations
23	Cole Schlesinger, Karthik Pattabiraman, Nikhil Swamy, David Walker 0001, Benjamin G. Zorn	Modular Protections against Non-control Data Attacks.	CSF	2011	DBLP DOI BibTeX RDF	non-control data attack, control-flow integrity, frame rule, data isolation, data integrity, Hoare logic, language-based security
23	Zhaopeng Li, Yang Zhang, Yiyun Chen	A Method to Generate Verification Condition Generator.	TASE	2011	DBLP DOI BibTeX RDF	Action Function, Program Verification, Hoare Logic, Verification Condition
23	Matthias Heizmann, Jochen Hoenicke, Andreas Podelski	Nested interpolants.	POPL	2010	DBLP DOI BibTeX RDF	floyd-hoare logic, nested words, static analysis, interpolants, abstract interpretation, recursion, software model checking, abstraction refinement
23	Aleksandar Nanevski, Viktor Vafeiadis, Josh Berdine	Structuring the verification of heap-manipulating programs.	POPL	2010	DBLP DOI BibTeX RDF	type theory, monads, hoare logic, separation logic
23	Aleksandar Nanevski, Paul Govereau, Greg Morrisett	Towards type-theoretic semantics for transactional concurrency.	TLDI	2009	DBLP DOI BibTeX RDF	type theory, monads, hoare logic, separation logic
23	Nurlida Basir, Ewen Denney, Bernd Fischer 0002	Constructing a Safety Case for Automatically Generated Code from Formal Program Verification Information.	SAFECOMP	2008	DBLP DOI BibTeX RDF	Goal Structuring Notation, Hoare logic, fault tree analysis, Automated code generation, safety case, formal program verification
23	James Brotherston, Richard Bornat, Cristiano Calcagno	Cyclic proofs of program termination in separation logic.	POPL	2008	DBLP DOI BibTeX RDF	cyclic proof, program verification, termination, hoare logic, separation logic, inductive definitions
23	Mohammad Raza, Philippa Gardner	Footprints in Local Reasoning.	FoSSaCS	2008	DBLP DOI BibTeX RDF	Hoare Logic, Separation Logic, Local Reasoning, Footprints
23	Ewen Denney, Bernd Fischer 0002	Generating customized verifiers for automatically generated code.	GPCE	2008	DBLP DOI BibTeX RDF	logical annotations, program verification, automated theorem proving, hoare logic, software certification, automated code generation
23	Aleksandar Nanevski, Greg Morrisett, Avraham Shinnar, Paul Govereau, Lars Birkedal	Ynot: dependent types for imperative programs.	ICFP	2008	DBLP DOI BibTeX RDF	type theory, monads, Hoare logic, separation logic
23	Steve M. Shaner, Gary T. Leavens, David A. Naumann	Modular verification of higher-order methods with mandatory calls specified by model programs.	OOPSLA	2007	DBLP DOI BibTeX RDF	grey-box approach, higher order method, mandatory call, model program, verification, specification languages, hoare logic, refinement calculus
23	Arthur Charlesworth	Comprehending software correctness implies comprehending an intelligence-related limitation.	ACM Trans. Comput. Log.	2006	DBLP DOI BibTeX RDF	Peano arithmetic, Zermelo-Fraenkel set theory, infallibility, partial correctness, Agent, consistency, soundness, Hoare logic, Turing machine, limitation, formal proof, halting problem
23	Marc Shapiro 0001	Practical proofs of concurrent programs.	ICFP	2006	DBLP DOI BibTeX RDF	concurrent programming, assertions, hoare logic, program proofs, rely-guarantee
23	Ralph-Johan Back, Viorel Preoteasa	An algebraic treatment of procedure refinement to support mechanical verification.	Formal Aspects Comput.	2005	DBLP DOI BibTeX RDF	Semantics, Refinement, Hoare logic, Recursive procedures, Mechanical verification
23	Alan Stewart, Maurice Clint, Joaquim Gabarró	Barrier synchronisation: Axiomatisation and relaxation.	Formal Aspects Comput.	2004	DBLP DOI BibTeX RDF	Global synchronisation, Operation relaxation, High performance computing, Hoare logic, BSP
23	Kohei Honda 0001	From process logic to program logic.	ICFP	2004	DBLP DOI BibTeX RDF	types, duality, hoare logic, ?-calculus, higher-order functions, mobile processes
23	Ewen Denney, Bernd Fischer 0002	Correctness of Source-Level Safety Policies.	FME	2003	DBLP DOI BibTeX RDF	program safety, code certification, Program verification, Hoare logic, proof-carrying code
23	Ralph-Johan Back, Viorel Preoteasa	Reasoning about recursive procedures with parameters.	MERLIN	2003	DBLP DOI BibTeX RDF	predicate transformer semantics, Hoare logic, refinement calculus, recursive procedures
23	Ian J. Hayes	Reasoning about real-time programs using idle-invariant assertions.	APSEC	2000	DBLP DOI BibTeX RDF	real-time program reasoning, idle-invariant assertions, software engineering, real-time systems, preconditions, formal logic, Hoare logic, postconditions
23	Luc Bougé, David Cachera	On the Completeness of a Proof System for a Simple Data-Parallel Programming Language.	Euro-Par	1995	DBLP DOI BibTeX RDF	Specifying and Verifying and Reasoning about Programs, Concurrent Programming, Hoare Logic, Weakest Preconditions, Proof System, Data-Parallel Languages, Semantics of Programming Languages
23	Donnacha Oisín Kidney, Zhixuan Yang, Nicolas Wu	Algebraic Effects Meet Hoare Logic in Cubical Agda.	Proc. ACM Program. Lang.	2024	DBLP DOI BibTeX RDF
23	Yusuke Kawamoto 0001, Tetsuya Sato 0001, Kohei Suenaga	Sound and relatively complete belief Hoare logic for statistical hypothesis testing programs.	Artif. Intell.	2024	DBLP DOI BibTeX RDF
23	Eduard Kamburjan, Dilian Gurov	A Hoare Logic for Domain Specification (Full Version).	CoRR	2024	DBLP DOI BibTeX RDF
23	Naijun Zhan, Bohua Zhan, Shuling Wang, Dimitar P. Guelev, Xiangyu Jin	A Generalized Hybrid Hoare Logic.	CoRR	2023	DBLP DOI BibTeX RDF
23	Roberto Metere, Changyu Dong	A Direct Lazy Sampling Proof Technique in Probabilistic Relational Hoare Logic.	CoRR	2023	DBLP DOI BibTeX RDF
23	Thibault Dardinier, Peter Müller 0001	Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version).	CoRR	2023	DBLP DOI BibTeX RDF
23	Johannes Åman Pohjola, Magnus O. Myreen, Miki Tanaka	A Hoare Logic for Diverging Programs.	Arch. Formal Proofs	2023	DBLP BibTeX RDF
23	Huanhuan Sheng, Alexander Bentkamp, Bohua Zhan	HHLPy: Practical Verification of Hybrid Systems Using Hoare Logic.	FM	2023	DBLP DOI BibTeX RDF
23	Gidon Ernst, Alexander Knapp, Toby Murray	A Hoare Logic with Regular Behavioral Specifications.	CoRR	2022	DBLP DOI BibTeX RDF
23	Joomy Korkut	A Proof Tree Builder for Sequent Calculus and Hoare Logic.	ThEdu@FLoC	2022	DBLP DOI BibTeX RDF
23	Yusuke Kawamoto 0001, Tetsuya Sato 0001, Kohei Suenaga	Sound and Relatively Complete Belief Hoare Logic for Statistical Hypothesis Testing Programs.	CoRR	2022	DBLP DOI BibTeX RDF
23	Huanhuan Sheng, Alexander Bentkamp, Bohua Zhan	HHLPy: Practical Verification of Hybrid Systems using Hoare Logic.	CoRR	2022	DBLP DOI BibTeX RDF
23	Anindya Banerjee 0001, Ramana Nagasamudram, David A. Naumann	Making Relational Hoare Logic Alignment Complete.	CoRR	2022	DBLP DOI BibTeX RDF
23	Gidon Ernst, Alexander Knapp, Toby Murray	A Hoare Logic with Regular Behavioral Specifications.	ISoLA (1)	2022	DBLP DOI BibTeX RDF
23	Zilin Chen	A Hoare logic style refinement types formalisation.	TyDe@ICFP	2022	DBLP DOI BibTeX RDF
23	Jan A. Bergstra, Cornelis A. Middelburg	Using Hoare Logic in a Process Algebra Setting.	Fundam. Informaticae	2021	DBLP DOI BibTeX RDF
23	Jayaraj Poroor	Natural Hoare Logic: Towards formal verification of programs from logical forms of natural language specifications.	CoRR	2021	DBLP BibTeX RDF
23	Boro Sitnikovski	Tutorial on implementing Hoare logic for imperative programs in Haskell.	CoRR	2021	DBLP BibTeX RDF
23	Frank S. de Boer, Hans-Dieter A. Hiep	Completeness and Complexity of Reasoning about Call-by-Value in Hoare Logic.	ACM Trans. Program. Lang. Syst.	2021	DBLP DOI BibTeX RDF
23	Yangjia Li, Dominique Unruh	Quantum Relational Hoare Logic with Expectations.	ICALP	2021	DBLP DOI BibTeX RDF