Results
Found 286 publication records. Showing 286 according to the selection in the facets
Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
105 | Thomas Kleymann |
Hoare Logic and Auxiliary Variables. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 11(5), pp. 541-566, 1999. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CSL ![In: Computer Science Logic, 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, Szeged, Hungary, September 25-29, 2006, Proceedings, pp. 501-515, 2006, Springer, 3-540-45458-6. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
82 | David von Oheimb, Tobias Nipkow |
Hoare Logic for NanoJava: Auxiliary Variables, Side Effects, and Virtual Methods Revisited. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FME ![In: FME 2002: Formal Methods - Getting IT Right, International Symposium of Formal Methods Europe, Copenhagen, Denmark, July 22-24, 2002, Proceedings, pp. 89-105, 2002, Springer, 3-540-43928-5. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FSTTCS ![In: Foundations of Software Technology and Theoretical Computer Science, 19th Conference, Chennai, India, December 13-15, 1999, Proceedings, pp. 168-180, 1999, Springer, 3-540-66836-5. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISICA ![In: Advances in Computation and Intelligence, 4th International Symposium, ISICA 2009, Huangshi, China, Ocotober 23-25, 2009, Proceedings, pp. 228-237, 2009, Springer, 978-3-642-04842-5. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Trans. Comput. Log. ![In: ACM Trans. Comput. Log. 1(1), pp. 60-76, 2000. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FMCO ![In: Formal Methods for Components and Objects, Second International Symposium, FMCO 2003, Leiden, The Netherlands, November 4-7, 2003, Revised Lectures, pp. 111-133, 2003, Springer, 3-540-22942-6. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
63 | Zhaozhong Ni, Zhong Shao |
Certified assembly programming with embedded code pointers. ![Search on Bibsonomy](Pics/bibsonomy.png) |
POPL ![In: Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, January 11-13, 2006, pp. 320-333, 2006, ACM, 1-59593-027-2. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LICS ![In: 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999, pp. 167-172, 1999, IEEE Computer Society, 0-7695-0158-3. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Trans. Comput. Log. ![In: ACM Trans. Comput. Log. 1(1), pp. 171-174, 2000. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
specification, Hoare logic |
57 | Cristiano Calcagno, Philippa Gardner, Uri Zarfaty |
Context logic and tree update. ![Search on Bibsonomy](Pics/bibsonomy.png) |
POPL ![In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005, pp. 271-282, 2005, ACM, 1-58113-830-X. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Frontiers Comput. Sci. China ![In: Frontiers Comput. Sci. China 1(3), pp. 297-312, 2007. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FSEN ![In: International Symposium on Fundamentals of Software Engineering, International Symposium, FSEN 2007, Tehran, Iran, April 17-19, 2007, Proceedings, pp. 272-286, 2007, Springer, 978-3-540-75697-2. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
49 | Hongxu Cai, Zhong Shao, Alexander Vaynberg |
Certified self-modifying code. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PLDI ![In: Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, San Diego, California, USA, June 10-13, 2007, pp. 66-77, 2007, ACM, 978-1-59593-633-2. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFP ![In: Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming, ICFP 2006, Portland, Oregon, USA, September 16-21, 2006, pp. 62-73, 2006, ACM, 1-59593-309-3. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Trans. Program. Lang. Syst. ![In: ACM Trans. Program. Lang. Syst. 29(6), pp. 39, 2007. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
POPL ![In: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004, Venice, Italy, January 14-16, 2004, pp. 14-25, 2004, ACM, 1-58113-729-X. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FASE ![In: Fundamental Approaches to Software Engineering, Third Internationsl Conference, FASE 2000, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS 2000, Berlin, Germany, March 25 - April 2, 2000, Proceedings, pp. 284-303, 2000, Springer, 3-540-67261-3. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP DOI BibTeX RDF |
|
46 | Jan Friso Groote, Alban Ponse |
Process Algebra with Guards - Combining Hoare Logic with Process Algebra (Extended Abstract). ![Search on Bibsonomy](Pics/bibsonomy.png) |
CONCUR ![In: CONCUR '91, 2nd International Conference on Concurrency Theory, Amsterdam, The Netherlands, August 26-29, 1991, Proceedings, pp. 235-249, 1991, Springer, 3-540-54430-5. The full citation details ...](Pics/full.jpeg) |
1991 |
DBLP DOI BibTeX RDF |
|
46 | Stephen L. Bloom, Zoltán Ésik |
Floyd-Hoare Logic in Iteration Theories. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. ACM ![In: J. ACM 38(4), pp. 887-934, 1991. The full citation details ...](Pics/full.jpeg) |
1991 |
DBLP DOI BibTeX RDF |
correction assertions, Hoare logic |
46 | Jerry den Hartog |
Verifying Probabilistic Programs Using a Hoare like Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ASIAN ![In: Advances in Computing Science - ASIAN'99, 5th Asian Computing Science Conference, Phuket, Thailand, December 10-12, 1999, Proceedings, pp. 113-125, 1999, Springer, 3-540-66856-X. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2312.09662, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
45 | Andreas Goerdt |
Hoare Logic for Lambda-Terms as Basis of Hoare Logic for Imperative Languages ![Search on Bibsonomy](Pics/bibsonomy.png) |
LICS ![In: Proceedings of the Symposium on Logic in Computer Science (LICS '87), Ithaca, New York, USA, June 22-25, 1987, pp. 293-299, 1987, IEEE Computer Society. The full citation details ...](Pics/full.jpeg) |
1987 |
DBLP BibTeX RDF |
|
45 | Cees Pierik, Frank S. de Boer |
A Syntax-Directed Hoare Logic for Object-Oriented Programming Concepts. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FMOODS ![In: Formal Methods for Open Object-Based Distributed Systems, 6th IFIP WG 6.1 International Conference, FMOODS 2003, Paris, France, November 19.21, 2003, Proceedings, pp. 64-78, 2003, Springer, 3-540-20491-1. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
40 | Matthew J. Parkinson, Richard Bornat, Cristiano Calcagno |
Variables as Resource in Hoare Logics. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LICS ![In: 21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings, pp. 137-146, 2006, IEEE Computer Society, 0-7695-2631-4. The full citation details ...](Pics/full.jpeg) |
2006 |
DBLP DOI BibTeX RDF |
|
39 | A. Udaya Shankar |
An Introduction to Assertional Reasoning for Concurrent Systems. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Comput. Surv. ![In: ACM Comput. Surv. 25(3), pp. 225-262, 1993. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
POPL ![In: Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, January 11-13, 2006, pp. 309-319, 2006, ACM, 1-59593-027-2. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MPC ![In: Mathematics of Program Construction, 9th International Conference, MPC 2008, Marseille, France, July 15-18, 2008. Proceedings, pp. 305-335, 2008, Springer, 978-3-540-70593-2. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
37 | Nadeem Abdul Hamid, Zhong Shao |
Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TPHOLs ![In: Theorem Proving in Higher Order Logics, 17th International Conference, TPHOLs 2004, Park City, Utah, USA, September 14-17, 2004, Proceedings, pp. 118-135, 2004, Springer, 3-540-23017-3. The full citation details ...](Pics/full.jpeg) |
2004 |
DBLP DOI BibTeX RDF |
|
36 | Andrew M. Gravell |
Verification conditions are code. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Acta Informatica ![In: Acta Informatica 43(6), pp. 431-447, 2007. The full citation details ...](Pics/full.jpeg) |
2007 |
DBLP DOI BibTeX RDF |
|
36 | Maria João Frade, Ando Saabas, Tarmo Uustalu |
Foundational certification of data-flow analyses. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TASE ![In: First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering, TASE 2007, June 5-8, 2007, Shanghai, China, pp. 107-116, 2007, IEEE Computer Society, 0-7695-2856-2. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
APLAS ![In: Programming Languages and Systems, First Asian Symposium, APLAS 2003, Beijing, China, November 27-29, 2003, Proceedings, pp. 230-245, 2003, Springer, 3-540-20536-5. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
35 | Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin |
Formal certification of code-based cryptographic proofs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
POPL ![In: Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009, pp. 90-101, 2009, ACM, 978-1-60558-379-2. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MCETECH ![In: E-Technologies: Innovation in an Open World, 4th International Conference, MCETECH 2009, Ottawa, Canada, May 4-6, 2009. Proceedings, pp. 252-266, 2009, Springer, 978-3-642-01186-3. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFEM ![In: Formal Methods and Software Engineering, 6th International Conference on Formal Engineering Methods, ICFEM 2004, Seattle, WA, USA, November 8-12, 2004, Proceedings, pp. 15-29, 2004, Springer, 3-540-23841-7. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Trans. Comput. Log. ![In: ACM Trans. Comput. Log. 4(3), pp. 355-378, 2003. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Trans. Comput. Log. ![In: ACM Trans. Comput. Log. 2(1), pp. 1-11, 2001. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
REX Workshop ![In: Foundations of Object-Oriented Languages, REX School/Workshop, Noordwijkerhout, The Netherlands, May 28 - June 1, 1990, Proceedings, pp. 124-150, 1990, Springer, 3-540-53931-X. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
IEEE Trans. Software Eng. ![In: IEEE Trans. Software Eng. 15(7), pp. 875-889, 1989. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Frontiers Comput. Sci. China ![In: Frontiers Comput. Sci. China 2(4), pp. 344-356, 2008. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TASE ![In: Second IEEE/IFIP International Symposium on Theoretical Aspects of Software Engineering, TASE 2008, June 17-19, 2008, Nanjing, China, pp. 151-158, 2008, IEEE Computer Society, 978-0-7695-3249-3. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
34 | Jean Yang 0001, Chris Hawblitzel |
Safe to the last instruction: automated verification of a type-safe operating system. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PLDI ![In: Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2010, Toronto, Ontario, Canada, June 5-10, 2010, pp. 99-110, 2010, ACM, 978-1-4503-0019-3. The full citation details ...](Pics/full.jpeg) |
2010 |
DBLP DOI BibTeX RDF |
verification, operating system, type safety, run-time system |
34 | Ando Saabas, Tarmo Uustalu |
Proof optimization for partial redundancy elimination. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PEPM ![In: Proceedings of the 2008 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation, PEPM 2008, San Francisco, California, USA, January 7-8, 2008, pp. 91-101, 2008, ACM, 978-1-59593-977-7. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CSFW ![In: 14th IEEE Computer Security Foundations Workshop (CSFW-14 2001), 11-13 June 2001, Cape Breton, Nova Scotia, Canada, pp. 241-255, 2001, IEEE Computer Society, 0-7695-1146-5. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FASE ![In: Fundamental Approaches to Software Engineering, 11th International Conference, FASE 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, pp. 199-214, 2008, Springer, 978-3-540-78742-6. The full citation details ...](Pics/full.jpeg) |
2008 |
DBLP DOI BibTeX RDF |
|
27 | Thibault Dardinier |
Formalization of Hyper Hoare Logic: A Logic to (Dis-)Prove Program Hyperproperties. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2023, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP BibTeX RDF |
|
27 | Yuan Feng 0001, Sanjiang Li |
Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Inf. Comput. ![In: Inf. Comput. 294, pp. 105077, October 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
27 | Yuan Feng 0001, Sanjiang Li |
Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2206.13772, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
27 | Jianhua Zhao, Xuandong Li |
Scope Logic: An Extension to Hoare Logic for Pointers and Recursive Data Structures. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICTAC ![In: Theoretical Aspects of Computing - ICTAC 2013 - 10th International Colloquium, Shanghai, China, September 4-6, 2013. Proceedings, pp. 409-426, 2013, Springer, 978-3-642-39717-2. The full citation details ...](Pics/full.jpeg) |
2013 |
DBLP DOI BibTeX RDF |
|
27 | Grigore Rosu, Andrei Stefanescu |
From Hoare Logic to Matching Logic Reachability. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FM ![In: FM 2012: Formal Methods - 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings, pp. 387-402, 2012, Springer, 978-3-642-32758-2. The full citation details ...](Pics/full.jpeg) |
2012 |
DBLP DOI BibTeX RDF |
|
27 | Jianhua Zhao, Xuandong Li |
Scope Logic: Extending Hoare Logic for Pointer Program Verification ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/0912.4184, 2009. The full citation details ...](Pics/full.jpeg) |
2009 |
DBLP BibTeX RDF |
|
27 | Andreas Blass, Yuri Gurevich |
The Underlying Logic of Hoare Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Current Trends in Theoretical Computer Science ![In: Current Trends in Theoretical Computer Science, Entering the 21th Century, pp. 409-436, 2001, World Scientific, 981-02-4473-8. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP BibTeX RDF |
|
27 | Andreas Blass, Yuri Gurevich |
The Underlying Logic of Hoare Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Bull. EATCS ![In: Bull. EATCS 70, pp. 82-111, 2000. The full citation details ...](Pics/full.jpeg) |
2000 |
DBLP BibTeX RDF |
|
27 | Peter M. W. Knijnenburg, Frank Nordemann |
Partial Hyperdoctrines: Categorical Models for Partial Function Logic and Hoare Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Math. Struct. Comput. Sci. ![In: Math. Struct. Comput. Sci. 4(2), pp. 117-146, 1994. The full citation details ...](Pics/full.jpeg) |
1994 |
DBLP DOI BibTeX RDF |
|
27 | Norbert E. Fuchs |
Hoare Logic, Executable Specifications and Logic Programs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Struct. Program. ![In: Struct. Program. 13(3), pp. 129-135, 1992. The full citation details ...](Pics/full.jpeg) |
1992 |
DBLP BibTeX RDF |
|
27 | Peter M. W. Knijnenburg, Frank Nordemann |
A Categorical Interpretation of Partial Function Logic and Hoare Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LFCS ![In: Logical Foundations of Computer Science - Tver '92, Second International Symposium, Tver, Russia, July 20-24, 1992, Proceedings, pp. 229-240, 1992, Springer, 3-540-55707-5. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
J. Autom. Reason. ![In: J. Autom. Reason. 42(2-4), pp. 301-347, 2009. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
PLDI ![In: Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7-13, 2008, pp. 170-182, 2008, ACM, 978-1-59593-860-2. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
HUG ![In: Higher Order Logic Theorem Proving and its Applications, 6th International Workshop, HUG '93, Vancouver, BC, Canada, August 11-13, 1993, Proceedings, pp. 29-42, 1993, Springer, 3-540-57826-9. The full citation details ...](Pics/full.jpeg) |
1993 |
DBLP DOI BibTeX RDF |
|
24 | Gordon D. Plotkin, Matija Pretnar |
A Logic for Algebraic Effects. ![Search on Bibsonomy](Pics/bibsonomy.png) |
LICS ![In: Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA, pp. 118-129, 2008, IEEE Computer Society, 978-0-7695-3183-0. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CSF ![In: Proceedings of the 24th IEEE Computer Security Foundations Symposium, CSF 2011, Cernay-la-Ville, France, 27-29 June, 2011, pp. 131-145, 2011, IEEE Computer Society, 978-1-61284-644-6. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TASE ![In: 5th IEEE International Symposium on Theoretical Aspects of Software Engineering, TASE 2011, Xi'an, China, 29-31 August 2011, pp. 239-242, 2011, IEEE Computer Society, 978-1-4577-1487-0. The full citation details ...](Pics/full.jpeg) |
2011 |
DBLP DOI BibTeX RDF |
Action Function, Program Verification, Hoare Logic, Verification Condition |
23 | Matthias Heizmann, Jochen Hoenicke, Andreas Podelski |
Nested interpolants. ![Search on Bibsonomy](Pics/bibsonomy.png) |
POPL ![In: Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010, pp. 471-482, 2010, ACM, 978-1-60558-479-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
POPL ![In: Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010, pp. 261-274, 2010, ACM, 978-1-60558-479-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TLDI ![In: Proceedings of TLDI'09: 2009 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation, Savannah, GA, USA, January 24, 2009, pp. 79-90, 2009, ACM, 978-1-60558-420-1. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
SAFECOMP ![In: Computer Safety, Reliability, and Security, 27th International Conference, SAFECOMP 2008, Newcastle upon Tyne, UK, September 22-25, 2008, Proceedings, pp. 249-262, 2008, Springer, 978-3-540-87697-7. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
POPL ![In: Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, San Francisco, California, USA, January 7-12, 2008, pp. 101-112, 2008, ACM, 978-1-59593-689-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FoSSaCS ![In: Foundations of Software Science and Computational Structures, 11th International Conference, FOSSACS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29 - April 6, 2008. Proceedings, pp. 201-215, 2008, Springer, 978-3-540-78497-5. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
GPCE ![In: Generative Programming and Component Engineering, 7th International Conference, GPCE 2008, Nashville, TN, USA, October 19-23, 2008, Proceedings, pp. 77-88, 2008, ACM, 978-1-60558-267-2. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFP ![In: Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, ICFP 2008, Victoria, BC, Canada, September 20-28, 2008, pp. 229-240, 2008, ACM, 978-1-59593-919-7. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
OOPSLA ![In: Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2007, October 21-25, 2007, Montreal, Quebec, Canada, pp. 351-368, 2007, ACM, 978-1-59593-786-5. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Trans. Comput. Log. ![In: ACM Trans. Comput. Log. 7(3), pp. 590-612, 2006. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFP ![In: Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming, ICFP 2006, Portland, Oregon, USA, September 16-21, 2006, pp. 123, 2006, ACM, 1-59593-309-3. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 17(1), pp. 69-90, 2005. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Formal Aspects Comput. ![In: Formal Aspects Comput. 16(1), pp. 36-50, 2004. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICFP ![In: Proceedings of the Ninth ACM SIGPLAN International Conference on Functional Programming, ICFP 2004, Snow Bird, UT, USA, September 19-21, 2004, pp. 163-174, 2004, ACM, 1-58113-905-5. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FME ![In: FME 2003: Formal Methods, International Symposium of Formal Methods Europe, Pisa, Italy, September 8-14, 2003, Proceedings, pp. 894-913, 2003, Springer, 3-540-40828-2. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: Eighth ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2003, Uppsala, Sweden, August 2003, 2003, ACM, 978-1-58113-800-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
APSEC ![In: 7th Asia-Pacific Software Engineering Conference (APSEC 2000), 5-8 December 2000, Singapore, pp. 16-23, 2000, IEEE Computer Society, 0-7695-0915-0. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Euro-Par ![In: Euro-Par '95 Parallel Processing, First International Euro-Par Conference, Stockholm, Sweden, August 29-31, 1995, Proceedings, pp. 143-154, 1995, Springer, 3-540-60247-X. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Proc. ACM Program. Lang. ![In: Proc. ACM Program. Lang. 8(POPL), pp. 1663-1695, January 2024. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Artif. Intell. ![In: Artif. Intell. 326, pp. 104045, January 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP DOI BibTeX RDF |
|
23 | Eduard Kamburjan, Dilian Gurov |
A Hoare Logic for Domain Specification (Full Version). ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2402.00452, 2024. The full citation details ...](Pics/full.jpeg) |
2024 |
DBLP DOI BibTeX RDF |
|
23 | Naijun Zhan, Bohua Zhan, Shuling Wang, Dimitar P. Guelev, Xiangyu Jin |
A Generalized Hybrid Hoare Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2303.15020, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
23 | Roberto Metere, Changyu Dong |
A Direct Lazy Sampling Proof Technique in Probabilistic Relational Hoare Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2311.16844, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
23 | Thibault Dardinier, Peter Müller 0001 |
Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties (extended version). ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2301.10037, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
23 | Johannes Åman Pohjola, Magnus O. Myreen, Miki Tanaka |
A Hoare Logic for Diverging Programs. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Arch. Formal Proofs ![In: Arch. Formal Proofs 2023, 2023. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP BibTeX RDF |
|
23 | Huanhuan Sheng, Alexander Bentkamp, Bohua Zhan |
HHLPy: Practical Verification of Hybrid Systems Using Hoare Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
FM ![In: Formal Methods - 25th International Symposium, FM 2023, Lübeck, Germany, March 6-10, 2023, Proceedings, pp. 160-178, 2023, Springer, 978-3-031-27480-0. The full citation details ...](Pics/full.jpeg) |
2023 |
DBLP DOI BibTeX RDF |
|
23 | Gidon Ernst, Alexander Knapp, Toby Murray |
A Hoare Logic with Regular Behavioral Specifications. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2205.06584, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
23 | Joomy Korkut |
A Proof Tree Builder for Sequent Calculus and Hoare Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ThEdu@FLoC ![In: Proceedings 11th International Workshop on Theorem Proving Components for Educational Software, ThEdu@FLoC 2022, Haifa, Israel, 11 August 2022., pp. 54-62, 2022. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2208.07074, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
23 | Huanhuan Sheng, Alexander Bentkamp, Bohua Zhan |
HHLPy: Practical Verification of Hybrid Systems using Hoare Logic. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2210.17163, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
23 | Anindya Banerjee 0001, Ramana Nagasamudram, David A. Naumann |
Making Relational Hoare Logic Alignment Complete. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2212.10338, 2022. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
23 | Gidon Ernst, Alexander Knapp, Toby Murray |
A Hoare Logic with Regular Behavioral Specifications. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ISoLA (1) ![In: Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles - 11th International Symposium, ISoLA 2022, Rhodes, Greece, October 22-30, 2022, Proceedings, Part I, pp. 45-64, 2022, Springer, 978-3-031-19848-9. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
23 | Zilin Chen |
A Hoare logic style refinement types formalisation. ![Search on Bibsonomy](Pics/bibsonomy.png) |
TyDe@ICFP ![In: TyDe '22: 7th ACM SIGPLAN International Workshop on Type-Driven Development, Ljubljana, Slovenia, 11 September 2022, pp. 1-14, 2022, ACM, 978-1-4503-9439-0. The full citation details ...](Pics/full.jpeg) |
2022 |
DBLP DOI BibTeX RDF |
|
23 | Jan A. Bergstra, Cornelis A. Middelburg |
Using Hoare Logic in a Process Algebra Setting. ![Search on Bibsonomy](Pics/bibsonomy.png) |
Fundam. Informaticae ![In: Fundam. Informaticae 179(4), pp. 321-344, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
23 | Jayaraj Poroor |
Natural Hoare Logic: Towards formal verification of programs from logical forms of natural language specifications. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2103.05779, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP BibTeX RDF |
|
23 | Boro Sitnikovski |
Tutorial on implementing Hoare logic for imperative programs in Haskell. ![Search on Bibsonomy](Pics/bibsonomy.png) |
CoRR ![In: CoRR abs/2101.11320, 2021. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ACM Trans. Program. Lang. Syst. ![In: ACM Trans. Program. Lang. Syst. 43(4), pp. 17:1-17:35, 2021. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
23 | Yangjia Li, Dominique Unruh |
Quantum Relational Hoare Logic with Expectations. ![Search on Bibsonomy](Pics/bibsonomy.png) |
ICALP ![In: 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, July 12-16, 2021, Glasgow, Scotland (Virtual Conference)., pp. 136:1-136:20, 2021, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 978-3-95977-195-5. The full citation details ...](Pics/full.jpeg) |
2021 |
DBLP DOI BibTeX RDF |
|
Displaying result #1 - #100 of 286 (100 per page; Change: ) Pages: [ 1][ 2][ 3][ >>] |