Found 30 Documents (Results 1–30)
Strong-separation logic. (English) Zbl 1473.03015
Yoshida, Nobuko (ed.), Programming languages and systems. 30th European symposium on programming, ESOP 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12648, 664-692 (2021).
Verified software units. (English) Zbl 1473.68035
Yoshida, Nobuko (ed.), Programming languages and systems. 30th European symposium on programming, ESOP 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12648, 118-147 (2021).
Connecting higher-order separation logic to a first-order outside world. (English) Zbl 1508.68070
Müller, Peter (ed.), Programming languages and systems. 29th European symposium on programming, ESOP 2020, held as part of the European joint conferences on theory and practice of software, ETAPS 2020, Dublin, Ireland, April 25–30, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12075, 428-455 (2020).
Abstraction and subsumption in modular verification of C programs. (English) Zbl 1539.68051
ter Beek, Maurice H. (ed.) et al., Formal methods – the next 30 years. Third world congress/23rd symposium, FM 2019, Porto, Portugal, October 7–11, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11800, 573-590 (2019).
Formalising mathematics in simple type theory. (English) Zbl 1528.03098
Centrone, Stefania (ed.) et al., Reflections on the foundations of mathematics. Univalent foundations, set theory and general thoughts. Based on the conference on foundations of mathematics: univalent foundations and set theory, FOMUS, Bielefeld, Germany, July 18–23, 2016. Cham: Springer. Synth. Libr. 407, 437-453 (2019).
On models of higher-order separation logic. (English) Zbl 1525.03093
Silva, Alexandra (ed.), Proceedings of the 33rd conference on the mathematical foundations of programming semantics (MFPS XXXIII), Ljubljana, Slovenia, June 12–15, 2017. Amsterdam: Elsevier. Electron. Notes Theor. Comput. Sci. 336, 57-78 (2018).
Iris from the ground up: a modular foundation for higher-order concurrent separation logic. (English) Zbl 1476.68062
Bringing order to the separation logic jungle. (English) Zbl 1503.03034
Chang, Bor-Yuh Evan (ed.), Programming languages and systems. 15th Asian symposium, APLAS 2017, Suzhou, China, November 27–29, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10695, 190-211 (2017).
Interactive proofs in higher-order concurrent separation logic. (English) Zbl 1380.68341
Castagna, Giuseppe (ed.) et al., Proceedings of the 44th annual ACM SIGPLAN symposium on principles of programming languages, POPL ’17, Paris, France, January 15–21, 2017. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-4660-3). 205-217 (2017).
The essence of higher-order concurrent separation logic. (English) Zbl 1485.68069
Yang, Hongseok (ed.), Programming languages and systems. 26th European symposium on programming, ESOP 2017, held as part of the European joint conferences on theory and practice of software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 10201, 696-723 (2017).
Transfinite step-indexing: decoupling concrete and logical steps. (English) Zbl 1335.68071
Thiemann, Peter (ed.), Programming languages and systems. 25th European symposium on programming, ESOP 2016, held as part of the European joint conferences on theory and practice of software, ETAPS 2016, Eindhoven, The Netherlands, April 2–8, 2016. Proceedings. Berlin: Springer (ISBN 978-3-662-49497-4/pbk; 978-3-662-49498-1/ebook). Lecture Notes in Computer Science 9632, 727-751 (2016).
Integrating linear and dependent types. (English) Zbl 1345.68109
Proceedings of the 42nd ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’15, Mumbai, India, January 12–18, 2015. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-3300-9). 17-30 (2015).
An operational and axiomatic semantics for non-determinism and sequence points in C. (English) Zbl 1284.68404
Proceedings of the 41st ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’14, San Diego, CA, USA, January 22–24, 2014. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-2544-8). 101-112 (2014).
Beyond 2-safety: asymmetric product programs for relational program verification. (English) Zbl 1419.68063
Artemov, Sergei (ed.) et al., Logical foundations of computer science. International symposium, LFCS 2013, San Diego, CA, USA, January 6–8, 2013. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 7734, 29-43 (2013).
A machine-checked framework for relational separation logic. (English) Zbl 1350.68059
Barthe, Gilles (ed.) et al., Software engineering and formal methods. 9th international conference, SEFM 2011, Montevideo, Uruguay, November 14–18, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-24689-0/pbk). Lecture Notes in Computer Science 7041, 122-137 (2011).
The rewriting logic semantics project: a progress report. (English) Zbl 1342.68198
Owe, Olaf (ed.) et al., Fundamentals of computation theory. 18th international symposium, FCT 2011, Oslo, Norway, August 22–25, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22952-7/pbk). Lecture Notes in Computer Science 6914, 1-37 (2011).
The relationship between separation logic and implicit dynamic frames. (English) Zbl 1326.68104
Barthe, Gilles (ed.), Programming languages and systems. 20th European symposium on programming, ESOP 2011, held as part of the joint European conferences on theory and practice of software, ETAPS 2011, Saarbrücken, Germany, March 26 – April 3, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-19717-8/pbk). Lecture Notes in Computer Science 6602, 439-458 (2011).
Barriers in concurrent separation logic. (English) Zbl 1326.68096
Barthe, Gilles (ed.), Programming languages and systems. 20th European symposium on programming, ESOP 2011, held as part of the joint European conferences on theory and practice of software, ETAPS 2011, Saarbrücken, Germany, March 26 – April 3, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-19717-8/pbk). Lecture Notes in Computer Science 6602, 276-296 (2011).
A formalisation of Smallfoot in HOL. (English) Zbl 1252.68266
Berghofer, Stefan (ed.) et al., Theorem proving in higher order logics. 22nd international conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-03358-2/pbk). Lecture Notes in Computer Science 5674, 469-484 (2009).
Practical tactics for separation logic. (English) Zbl 1252.68261
Berghofer, Stefan (ed.) et al., Theorem proving in higher order logics. 22nd international conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-03358-2/pbk). Lecture Notes in Computer Science 5674, 343-358 (2009).
MSC:
68T15
03B70
Formal verification of C systems code. Structured types, separation logic and theorem proving. (English) Zbl 1191.68417
Multimodal separation logic for reasoning about operational semantics. (English) Zbl 1286.68395
Bauer, Andrej (ed.) et al., Proceedings of the 24th conference on the mathematical foundations of programming semantics (MFPS XXIV), Philadelphia, PA, USA, May 22–25, 2008. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 218, 5-20 (2008).
Filter Results by …
Document Type
- Journal Articles (10)
- Collection Articles (20)
all
top 5
Author
- Appel, Andrew W. (6)
- Krebbers, Robbert (6)
- Birkedal, Lars (5)
- Beringer, Lennart (4)
- Bizjak, Aleš (3)
- Bengtson, Jesper (2)
- Cao, Qinxiang (2)
- Crespo, Juan Manuel (2)
- Dreyer, Derek R. (2)
- Hobor, Aquinas (2)
- Jourdan, Jacques-Henri (2)
- Jung, Ralf (2)
- Kunz, César (2)
- Meseguer Guaita, José (2)
- Pagel, Jens (2)
- Roşu, Grigore (2)
- Zuleger, Florian (2)
- Barthe, Gilles (1)
- Benton, Nick (1)
- Cuellar, Santiago (1)
- Dockins, Robert (1)
- Doczkal, Christian (1)
- Dodds, Josiah (1)
- Gherghina, Cristian (1)
- Grütter, Samuel (1)
- Honoré, Wolf (1)
- Kastberg Hinrichsen, Jonas (1)
- Krishnaswami, Neelakantan R. (1)
- Mansky, William (1)
- Matheja, Christoph (1)
- McCreight, Andrew (1)
- Parkinson, Matthew J. (1)
- Paulson, Lawrence Charles (1)
- Paviotti, Marco (1)
- Pradic, Pierre (1)
- Sieczkowski, Filip (1)
- Smolka, Gert (1)
- Summers, Alexander J. (1)
- Svendsen, Kasper (1)
- Timany, Amin (1)
- Tuch, Harvey (1)
- Tuerk, Thomas (1)
all
top 3
Software
- Coq (17)
- Toolchain (12)
- cminor (7)
- Isabelle/HOL (4)
- VeriFast (4)
- CompCert (3)
- Dafny (3)
- RustBelt (3)
- Smallfoot (3)
- VST-Floyd (3)
- ACL2 (2)
- Bedrock (2)
- Centaur (2)
- Charge! (2)
- CompCertTSO (2)
- Coq/SSReflect (2)
- Dist-Orc (2)
- Frama-C (2)
- GitHub (2)
- HIP (2)
- ITP/OCL (2)
- Java+ITP (2)
- JavaFAN (2)
- K Prover (2)
- K tool (2)
- KRAKATOA (2)
- MMT (2)
- MOMENT2 (2)
- Maude (2)
- Rust (2)
- VCC (2)
- ACSL (1)
- Agda (1)
- Automath (1)
- BLAST (1)
- Boogie (1)
- CBMC (1)
- CIL (1)
- Caduceus (1)
- CafeOBJ (1)
- Cambridge LCF (1)
- CertiKOS (1)
- CoVaC (1)
- Coquelicot (1)
- EasyCrypt (1)
- Finite Automata HF (1)
- Flocq (1)
- GRASShopper (1)
- HOL Light (1)
- Hereditarily Finite Sets (1)
- Infer (1)
- Isabelle (1)
- ML (1)
- MSO_Regex_Equivalence (1)
- MapReduce (1)
- Mechanized Semantic Library (1)
- Mizar (1)
- MoSeL (1)
- Myhill-Nerode (1)
- Nuprl (1)
- Orc (1)
- PMaude (1)
- PVeStA (1)
- PoplMark (1)
- Presburger Automata (1)
- Ptolemy (1)
- Regular Sets (1)
- SLAyer (1)
- Slide (1)
- TVOC (1)
- TweetNaCl (1)
- Viper (1)
- Why3 (1)
- pthreads (1)
- seL4 (1)
- vlogsl (1)
