×

Found 25 Documents (Results 1–25)

Making theory reasoning simpler. (English) Zbl 1474.68060

Groote, Jan Friso (ed.) et al., Tools and algorithms for the construction and analysis of systems. 27th international conference, TACAS 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. Part II. Cham: Springer. Lect. Notes Comput. Sci. 12652, 164-180 (2021).
MSC:  68N30 68T20
PDFBibTeX XMLCite
Full Text: DOI

ConSORT: context- and flow-sensitive ownership refinement types for imperative programs. (English) Zbl 1508.68079

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, 684-714 (2020).
MSC:  68N30 68N18 68Q60
PDFBibTeX XMLCite
Full Text: DOI arXiv

Loop analysis by quantification over iterations. (English) Zbl 1415.68146

Barthe, Gilles (ed.) et al., LPAR-22. 22nd international conference on logic for programming, artificial intelligence and reasoning, Awassa, Ethiopia, November 17–21, 2018. Selected papers. Manchester: EasyChair. EPiC Ser. Comput. 57, 381-399 (2018).
MSC:  68Q60 68N30
PDFBibTeX XMLCite
Full Text: DOI Link

Symbolic computation via program transformation. (English) Zbl 1518.68055

Fischer, Bernd (ed.) et al., Theoretical aspects of computing – ICTAC 2018. 15th international colloquium, Stellenbosch, South Africa, October 16–19, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 11187, 313-332 (2018).
PDFBibTeX XMLCite
Full Text: DOI arXiv

A FOOLish encoding of the next state relations of imperative programs. (English) Zbl 1511.68160

Galmiche, Didier (ed.) et al., Automated reasoning. 9th international joint conference, IJCAR 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 14–17, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10900, 405-421 (2018).
MSC:  68Q60 68N30 68V15
PDFBibTeX XMLCite
Full Text: DOI

Effective use of SMT solvers for program equivalence checking through invariant-sketching and query-decomposition. (English) Zbl 1511.68312

Beyersdorff, Olaf (ed.) et al., Theory and applications of satisfiability testing – SAT 2018. 21st international conference, SAT 2018, held as part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9–12, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10929, 365-382 (2018).
MSC:  68V15 68N30 68Q60
PDFBibTeX XMLCite
Full Text: DOI

LOIS: syntax and semantics. (English) Zbl 1380.68125

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). 586-598 (2017).
MSC:  68N30 68N15 68Q55
PDFBibTeX XMLCite
Full Text: DOI

Coming to terms with quantified reasoning. (English) Zbl 1380.68280

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). 260-270 (2017).
MSC:  68Q60 68N30 68T15
PDFBibTeX XMLCite
Full Text: DOI arXiv

Partitioned memory models for program analysis. (English) Zbl 1484.68054

Bouajjani, Ahmed (ed.) et al., Verification, model checking, and abstract interpretation. 18th international conference, VMCAI 2017, Paris, France, January 15–17, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10145, 539-558 (2017).
MSC:  68N30 68P05
PDFBibTeX XMLCite
Full Text: DOI

Polyhedral approximation of multivariate polynomials using Handelman’s theorem. (English) Zbl 1475.68093

Jobstmann, Barbara (ed.) et al., Verification, model checking, and abstract interpretation. 17th international conference, VMCAI 2016, St. Petersburg, FL, USA, January 17–19, 2016. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 9583, 166-184 (2016).
PDFBibTeX XMLCite
Full Text: DOI HAL

A first class Boolean sort in first-order theorem proving and TPTP. (English) Zbl 1417.68187

Kerber, Manfred (ed.) et al., Intelligent computer mathematics. International conference, CICM 2015, Washington, DC, USA, July 13–17, 2015, Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9150, 71-86 (2015).
MSC:  68T15 68N30
PDFBibTeX XMLCite
Full Text: DOI arXiv

Modular reasoning about heap paths via effectively propositional formulas. (English) Zbl 1284.68403

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). 385-396 (2014).
PDFBibTeX XMLCite
Full Text: DOI

Definability of accelerated relations in a theory of arrays and its applications. (English) Zbl 1397.68121

Fontaine, Pascal (ed.) et al., Frontiers of combining systems. 9th international symposium, FroCoS 2013, Nancy, France, September 18–20, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-40884-7/pbk). Lecture Notes in Computer Science 8152. Lecture Notes in Artificial Intelligence, 23-39 (2013).
MSC:  68Q60 03B70 68N30
PDFBibTeX XMLCite
Full Text: DOI arXiv

Playing in the grey area of proofs. (English) Zbl 1321.68196

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). 259-272 (2012).
MSC:  68N30 68T15
PDFBibTeX XMLCite
Full Text: DOI

Dafny: an automatic program verifier for functional correctness. (English) Zbl 1253.68095

Clarke, Edmund M. (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 16th international conference, LPAR-16, Dakar, Senegal, April 25 – May 1, 2010. Revised selected papers. Berlin: Springer (ISBN 978-3-642-17510-7/pbk). Lecture Notes in Computer Science 6355. Lecture Notes in Artificial Intelligence, 348-370 (2010).
MSC:  68N30 68Q60
PDFBibTeX XMLCite
Full Text: DOI

Unifying type checking and property checking for low-level code. (English) Zbl 1315.68086

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). 302-314 (2009).
MSC:  68N30 68N15
PDFBibTeX XMLCite
Full Text: DOI

Towards modular algebraic specifications for pointer programs: A case study. (English) Zbl 1186.68116

Comon-Lundh, Hubert (ed.) et al., Rewriting, computation and proof. Essays dedicated to Jean-Pierre Jouannaud on the occasion of his 60th birthday. Berlin: Springer (ISBN 978-3-540-73146-7/pbk). Lecture Notes in Computer Science 4600, 235-258 (2007).
MSC:  68N30 68Q65
PDFBibTeX XMLCite
Full Text: DOI

Filter Results by …

Document Type

all top 5

Year of Publication

all top 3

Main Field

all top 3

Software