×

Found 239 Documents (Results 1–100)

100
MathJax

Weakest preconditions in fibrations. (English) Zbl 07516369

Johann, Patricia (ed.), Proceedings of the 36th conference on mathematical foundations of programming semantics, MFPS XXXVI, virtual conference, June 2–6, 2020. Amsterdam: Elsevier. Electron. Notes Theor. Comput. Sci. 352, 5-27 (2020).
MSC:  68N30 68Q55
PDF BibTeX XML Cite
Full Text: DOI

Hoare-style logic for unstructured programs. (English) Zbl 1476.68064

de Boer, Frank (ed.) et al., Software engineering and formal methods. 18th international conference, SEFM 2020, Amsterdam, The Netherlands, September 14–18, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12310, 193-213 (2020).
MSC:  68N30 03B70 68V15
PDF BibTeX XML Cite
Full Text: DOI Link

Formal verification of Ethereum smart contracts using Isabelle/HOL. (English) Zbl 1476.68156

Nigam, Vivek (ed.) et al., Logic, language, and security. Essays dedicated to Andre Scedrov on the occasion of his 65th birthday. Cham: Springer. Lect. Notes Comput. Sci. 12300, 71-97 (2020).
PDF BibTeX XML Cite
Full Text: DOI

Concurrent separation logic meets template games. (English) Zbl 07299509

Proceedings of the 2020 35th annual ACM/IEEE symposium on logic in computer science, LICS 2020, virtual event, July 8–11, 2020. New York, NY: Association for Computing Machinery (ACM). 742-755 (2020).
MSC:  68-XX 03B70
PDF BibTeX XML Cite
Full Text: DOI arXiv

Indexed and fibred structures for Hoare logic. (English) Zbl 07297795

Felty, Amy (ed.) et al., 14th international workshop on logical and semantic frameworks, with applications, LSFA 2019, Natal, Brazil, in August 2019. Amsterdam: Elsevier. Electron. Notes Theor. Comput. Sci. 348, 125-145 (2020).
MSC:  03B70 03G30 18N45
PDF BibTeX XML Cite
Full Text: DOI

Starvation-free monitors. (English) Zbl 07142676

Hierons, Robert Mark (ed.) et al., Theoretical aspects of computing – ICTAC 2019. 16th international colloquium, Hammamet, Tunisia, October 31 – November 4, 2019. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11884, 175-195 (2019).
MSC:  68Qxx
PDF BibTeX XML Cite
Full Text: DOI Link

Hoare logics for time bounds. A study in meta theory. (English) Zbl 1423.68098

Beyer, Dirk (ed.) et al., Tools and algorithms for the construction and analysis of systems. 24th international conference, TACAS 2018, held as part of the European joint conferences on theory and practice of software, ETAPS 2018, Thessaloniki, Greece, April 14–20, 2018. Proceedings. Part I. Cham: Springer. Lect. Notes Comput. Sci. 10805, 155-171 (2018).
MSC:  68N30 03B70 68Q60 68T15 68W40
PDF BibTeX XML Cite
Full Text: DOI

Coupling proofs are probabilistic product programs. (English) Zbl 1380.68267

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). 161-174 (2017).
MSC:  68Q60 03B70 68N30
PDF BibTeX XML Cite
Full Text: DOI arXiv

Completeness of Hoare logic relative to the standard model. (English) Zbl 1444.03122

Steffen, Bernhard (ed.) et al., SOFSEM 2017: theory and practice of computer science. 43rd international conference on current trends in theory and practice of computer science, Limerick, Ireland, January 16–20, 2017, Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10139, 119-131 (2017).
MSC:  03B70 03C62 03F30
PDF BibTeX XML Cite
Full Text: DOI arXiv

A sound and complete Hoare logic for dynamically-typed, object-oriented programs. (English) Zbl 1475.68085

Ábrahám, Erika (ed.) et al., Theory and practice of formal methods. Essays dedicated to Frank de Boer on the occasion of his 60th birthday. Cham: Springer. Lect. Notes Comput. Sci. 9660, 173-193 (2016).
PDF BibTeX XML Cite
Full Text: DOI arXiv

Relational logic with framing and hypotheses. (English) Zbl 1391.68017

Lal, Akash (ed.) et al., 36th IARCS annual conference on foundations of software technology and theoretical computer science (FSTTCS 2016), Chennai, India, December 13–15, 2016. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-95977-027-9). LIPIcs – Leibniz International Proceedings in Informatics 65, Article 11, 16 p. (2016).
MSC:  68N30 03B70 68Q60
PDF BibTeX XML Cite
Full Text: DOI arXiv

A program logic for union bounds. (English) Zbl 1388.68022

Chatzigiannakis, Ioannis (ed.) et al., 43rd international colloquium on automata, languages, and programming, ICALP 2016, Rome, Italy, July 12–15, 2016. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-95977-013-2). LIPIcs – Leibniz International Proceedings in Informatics 55, Article 107, 15 p. (2016).
MSC:  68N30 03B70 68Q87
PDF BibTeX XML Cite
Full Text: DOI arXiv

Proving correctness of logically decorated graph rewriting systems. (English) Zbl 1387.68144

Kesner, Delia (ed.) et al., 1st international conference on formal structures for computation and deduction, FSCD 2016, Porto, Portugal, June 22–26, 2016. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-95977-010-1). LIPIcs – Leibniz International Proceedings in Informatics 52, Article 14, 15 p. (2016).
MSC:  68Q42 03B70 68N30
PDF BibTeX XML Cite
Full Text: DOI

VPHL: a verified partial-correctness logic for probabilistic programs. (English) Zbl 1351.68080

Ghica, Dan (ed.), Proceedings of the 31st conference on the mathematical foundations of programming semantics (MFPS XXXI), Nijmegen, The Netherlands, June 22–25, 2015. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 319, 351-367, electronic only (2015).
PDF BibTeX XML Cite
Full Text: DOI

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).
PDF BibTeX XML Cite
Full Text: DOI

Formal verification of Simulink/Stateflow diagrams. (English) Zbl 1471.68159

Finkbeiner, Bernd (ed.) et al., Automated technology for verification and analysis. 13th international symposium, ATVA 2015, Shanghai, China, October 12–15, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9364, 464-481 (2015).
PDF BibTeX XML Cite
Full Text: DOI

On the Hoare theory of monadic recursion schemes. (English) Zbl 1401.68045

Proceedings of the joint meeting of the twenty-third EACSL annual conference on computer science logic, CSL, and the 2014 29th annual ACM/IEEE symposium on logic in computer science, LICS 2014, Vienna, Austria, July 14–18, 2014. Los Alamitos, CA: IEEE Computer Society (ISBN 978-1-4503-2886-9). Paper No. 69, 10 p. (2014).
MSC:  68N30 03B25 03B70
PDF BibTeX XML Cite
Full Text: DOI Link

Summary-based inter-procedural analysis via modular trace refinement. (English) Zbl 1360.68581

Raman, Venkatesh (ed.) et al., 34th international conference on foundation of software technology and theoretical computer science, FSTTCS 2014, New Delhi, India, December 15–17, 2014. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-77-4). LIPIcs – Leibniz International Proceedings in Informatics 29, 545-556 (2014).
MSC:  68Q60 68Q45
PDF BibTeX XML Cite
Full Text: DOI

Program logics for certified compilers. (English) Zbl 1298.68009

Cambridge: Cambridge University Press (ISBN 978-1-107-04801-0/hbk; 978-1-107-25655-2/ebook). x, 458 p. (2014).
PDF BibTeX XML Cite
Full Text: DOI

One-path reachability logic. (English) Zbl 1366.68182

Proceedings of the 2013 28th annual ACM/IEEE symposium on logic in computer science, LICS 2013, Tulane University, New Orleans, LA, USA, June 25–28, 2013. Los Alamitos, CA: IEEE Computer Society (ISBN 978-0-7695-5020-6). 358-367 (2013).
PDF BibTeX XML Cite
Full Text: DOI

A relatively complete generic Hoare logic for order-enriched effects. (English) Zbl 1366.68023

Proceedings of the 2013 28th annual ACM/IEEE symposium on logic in computer science, LICS 2013, Tulane University, New Orleans, LA, USA, June 25–28, 2013. Los Alamitos, CA: IEEE Computer Society (ISBN 978-0-7695-5020-6). 273-282 (2013).
PDF BibTeX XML Cite
Full Text: DOI

Formal modelling, analysis and verification of hybrid systems. (English) Zbl 1444.68105

Liu, Zhiming (ed.) et al., Unifying theories of programming and formal engineering methods. International training school on software engineering, held at ICTAC 2013, Shanghai, China, August 26–30, 2013. Advanced lectures. Berlin: Springer. Lect. Notes Comput. Sci. 8050, 207-281 (2013).
PDF BibTeX XML Cite
Full Text: DOI Link

Hoare-style reasoning with (algebraic) continuations. (English) Zbl 1323.68369

Proceedings of the 18th ACM SIGPLAN international conference on functional programming, ICFP ’13, Boston, MA, USA, September 25–27, 2013. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-2326-0). ACM SIGPLAN Notices 48, No. 9, 363-376 (2013).
MSC:  68Q60 03B70 68N30
PDF BibTeX XML Cite
Full Text: DOI Link

Logic calculi in informatics. How is logic used by the computer? (Logikkalküle in der Informatik. Wie wird Logik vom Rechner genutzt?) (German) Zbl 1296.03001

Studienbücher Informatik. Wiesbaden: Springer Vieweg (ISBN 978-3-8348-1887-4/pbk; 978-3-8348-2295-6/ebook). xii, 232 p. (2013).
PDF BibTeX XML Cite
Full Text: DOI

Graph-based object-oriented Hoare logic. (English) Zbl 1390.68192

Liu, Zhiming (ed.) et al., Theories of programming and formal methods. Essays dedicated to Jifeng He on the occasion of his 70th birthday. Berlin: Springer (ISBN 978-3-642-39697-7/pbk). Lecture Notes in Computer Science 8051, 374-393 (2013).
PDF BibTeX XML Cite
Full Text: DOI

Probabilistic relational reasoning for differential privacy. (English) Zbl 1321.68182

Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’12, Philadelphia, PA, USA, January 22–28, 2012. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-1083-3). 97-110 (2012).
MSC:  68N30 94A60 68T15 68W20 68W27
PDF BibTeX XML Cite
Full Text: DOI Link

Reverse exchange for concurrency and local reasoning. (English) Zbl 1358.68063

Gibbons, Jeremy (ed.) et al., Mathematics of program construction. 11th international conference, MPC 2012, Madrid, Spain, June 25–27, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-31112-3/pbk). Lecture Notes in Computer Science 7342, 177-197 (2012).
MSC:  68N19 03B70
PDF BibTeX XML Cite
Full Text: DOI Link

An assume/guarantee based compositional calculus for hybrid CSP. (English) Zbl 1354.68204

Agrawal, Manindra (ed.) et al., Theory and applications of models of computation. 9th annual conference, TAMC 2012, Beijing, China, May 16–21, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-29951-3/pbk). Lecture Notes in Computer Science 7287, 72-83 (2012).
MSC:  68Q85 03B70 68Q60
PDF BibTeX XML Cite
Full Text: DOI

Conditional reactive systems. (English) Zbl 1246.68152

Chakraborthy, Supraik (ed.) et al., IARCS annual conference on foundations of software technology and theoretical computer science (FSTTCS 2011), Mumbai, India, December 12–14, 2011. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik (ISBN 978-3-939897-34-7). LIPIcs – Leibniz International Proceedings in Informatics 13, 191-203, electronic only (2011).
MSC:  68Q60 03B70 68Q42
PDF BibTeX XML Cite
Full Text: DOI

Hoare logic for higher order store using simple semantics. (English) Zbl 1326.68085

Beklemishev, Lev D. (ed.) et al., Logic, language, information and computation. 18th international workshop, WoLLIC 2011, Philadelphia, PA, USA, May 18–20, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-20919-2/pbk). Lecture Notes in Computer Science 6642. Lecture Notes in Artificial Intelligence, 52-66 (2011).
MSC:  68N30 03B70
PDF BibTeX XML Cite
Full Text: DOI

Concurrency verification. Introduction to compositional and noncompositional methods. Reprint of the 2001 hardback ed. (English) Zbl 1214.68125

Cambridge Tracts in Theoretical Computer Science 54. Cambridge: Cambridge University Press (ISBN 978-0-521-16932-5/pbk). xxii, 776 p. (2011).
PDF BibTeX XML Cite

Nested interpolants. (English) Zbl 1312.68059

Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’10, Madrid, Spain, January 17–23, 2010. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-60558-479-9). 471-482 (2010).
MSC:  68N30 68Q60
PDF BibTeX XML Cite
Full Text: DOI

Structuring the verification of heap-manipulating programs. (English) Zbl 1312.68065

Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’10, Madrid, Spain, January 17–23, 2010. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-60558-479-9). 261-274 (2010).
MSC:  68N30
PDF BibTeX XML Cite
Full Text: DOI

Mechanized semantics. With applications to program proof and compiler verification. (English) Zbl 1213.68206

Esparza, Javier (ed.) et al., Logics and languages for reliability and security. Selected papers based on the presentations at the 30th international summer school, Marktoberdorf, Germany, August 4–16, 2009. Amsterdam: IOS Press (ISBN 978-1-60750-099-5/hbk; 978-1-60750-100-8/ebook). NATO Science for Peace and Security Series D: Information and Communication Security 25, 195-224 (2010).
MSC:  68N30 68N20 68Q55 68T15
PDF BibTeX XML Cite
Full Text: DOI arXiv

Forward with Hoare. (English) Zbl 1215.68129

Jones, Cliff B. (ed.) et al., Reflections on the work of C. A. R. Hoare. Most papers based on the presentations at the meeting to celebrate Tony Hoare’s 75th birthday, Cambridge, UK, April 2009. London: Springer (ISBN 978-1-84882-911-4/hbk; 978-1-84882-912-1/ebook). 101-121 (2010).
MSC:  68Q60 68N30 03B70
PDF BibTeX XML Cite
Full Text: DOI

Separation logic and concurrency. (English) Zbl 1200.68066

Boca, Paul P. (ed.) et al., Formal methods: State of the art and new directions. Dedicated to Peter Landin (1930–2009). London: Springer (ISBN 978-1-84882-735-6/hbk; 978-1-84882-736-3/ebook). 217-248 (2010).
MSC:  68N19
PDF BibTeX XML Cite
Full Text: DOI Link

Inductive completeness of logics of programs. (English) Zbl 1234.03018

Abel, Andreas (ed.) et al., Proceedings of the 3rd international workshop on logical frameworks and metalanguages: theory and practice (LFMTP 2008), Pittsburgh, PA, USA, June 23, 2008. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 228, 101-112 (2009).
MSC:  03B70 68N30
PDF BibTeX XML Cite
Full Text: DOI

Formal certification of code-based cryptographic proofs. (English) Zbl 1315.68081

Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’09, Savannah, GA, USA, January 18–24, 2009. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-60558-379-2). 90-101 (2009).
MSC:  68N30 03B70 68T15 94A60
PDF BibTeX XML Cite
Full Text: DOI Link

Formative E-assessment in university teaching. Computer-aided control of the progress of learning in the study of informatics. (Formatives E-Assessment in der Hochschullehre. Computerunterstützte Lernfortschrittskontrollen im Informatikstudium.) (German) Zbl 1189.00023

Münster: Univ. Münster, Mathematisch-Naturwissenschaftliche Fakultät, Fachbereich Mathematik und Informatik (Diss.). xiv, 265 p. (2009).
PDF BibTeX XML Cite

Ynot: dependent types for imperative programs. (English) Zbl 1323.68142

Proceedings of the 13th ACM SIGPLAN international conference on functional programming, ICFP ’08, Victoria, BC, Canada, September 20–28, 2008. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-59593-919-7). ACM SIGPLAN Notices 43, No. 9, 229-240 (2008).
MSC:  68N18 03B70 68N15 68T15
PDF BibTeX XML Cite
Full Text: DOI

Cyclic proofs of program termination in separation logic. (English) Zbl 1295.68156

Proceedings of the 35th ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’08, San Francisco, CA, USA, January 07–12, 2008. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-59593-689-9). 101-112 (2008).
PDF BibTeX XML Cite
Full Text: DOI

On formal certification of AD transformations. (English) Zbl 1156.68572

Bischof, Christian H. (ed.) et al., Advances in automatic differentiation. Selected papers based on the presentations at the 5th international conference on automatic differentiation, Bonn, Germany, August 11–15, 2008. Berlin: Springer (ISBN 978-3-540-68935-5/pbk). Lecture Notes in Computational Science and Engineering 64, 23-33 (2008).
MSC:  68T15 68N30
PDF BibTeX XML Cite

Footprints in local reasoning. (English) Zbl 1139.68020

Amadio, Roberto (ed.), 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. Berlin: Springer (ISBN 978-3-540-78497-5/pbk). Lecture Notes in Computer Science 4962, 201-215 (2008).
MSC:  68N30 03B70
PDF BibTeX XML Cite
Full Text: DOI arXiv

Building verification condition generators by compositional extension. (English) Zbl 1277.68062

Romijn, Judi (ed.) et al., Proceedings of the doctoral symposium affiliated with the fifth integrated formal methods conference (IFM 2005), Eindhoven, The Netherlands, November 29, 2005. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 191, 73-83 (2007).
MSC:  68N30 03B70 68Q55
PDF BibTeX XML Cite
Full Text: DOI

Certified assembly programming with embedded code pointers. (English) Zbl 1369.68150

Proceedings of the 33rd ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’06, Charleston, SC, USA, January 11–13, 2006. New York, NY: Association for Computing Machinery (ACM) (ISBN 1-59593-027-2). 320-333 (2006).
MSC:  68N30 68T15
PDF BibTeX XML Cite
Full Text: DOI

Filter Results by …

Document Type

Reviewing State

all top 5

Author

all top 5

Year of Publication

all top 3

Classification

all top 3

Software