×

Found 466 Documents (Results 1–100)

100
MathJax

Automatic generation and validation of instruction encoders and decoders. (English) Zbl 1493.68223

Silva, Alexandra (ed.) et al., Computer aided verification. 33rd international conference, CAV 2021, virtual event, July 20–23, 2021. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 12760, 728-751 (2021).
MSC:  68Q60 68N30 68V15
PDF BibTeX XML Cite
Full Text: DOI

Towards a trustworthy semantics-based language framework via proof generation. (English) Zbl 1493.68056

Silva, Alexandra (ed.) et al., Computer aided verification. 33rd international conference, CAV 2021, virtual event, July 20–23, 2021. Proceedings. Part II. Cham: Springer. Lect. Notes Comput. Sci. 12760, 477-499 (2021).
MSC:  68N15 03B70 68Q60
PDF BibTeX XML Cite
Full Text: DOI

Event-B-supported choreography-defined communicating systems. (English) Zbl 07602231

Raschke, Alexander (ed.) et al., Rigorous state-based methods. 7th international conference, ABZ 2020, Ulm, Germany, May 27–29, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12071, 155-168 (2020).
MSC:  68Q85 68Q60
PDF BibTeX XML Cite
Full Text: DOI

Equality checking for general type theories in Andromeda 2. (English) Zbl 07600897

Bigatti, Anna Maria (ed.) et al., Mathematical software – ICMS 2020. 7th international conference, Braunschweig, Germany, July 13–16, 2020. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12097, 253-259 (2020).
MSC:  65Yxx 68Vxx 68W30
PDF BibTeX XML Cite
Full Text: DOI

Affine systems of ODEs in Isabelle/HOL for hybrid-program verification. (English) Zbl 1476.68301

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, 77-92 (2020).
MSC:  68V20 34A30 68Q60
PDF BibTeX XML Cite
Full Text: DOI

Local verification of global proofs. (English) Zbl 07561277

Schmid, Ulrich (ed.) et al., 32nd international symposium on distributed computing, DISC 2018, New Orleans, Louisiana, USA, October 15–19, 2018. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 121, Article 25, 17 p. (2018).
PDF BibTeX XML Cite
Full Text: DOI arXiv

Redundancy in distributed proofs. (English) Zbl 07561276

Schmid, Ulrich (ed.) et al., 32nd international symposium on distributed computing, DISC 2018, New Orleans, Louisiana, USA, October 15–19, 2018. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. LIPIcs – Leibniz Int. Proc. Inform. 121, Article 24, 18 p. (2018).
PDF BibTeX XML Cite
Full Text: DOI

LMSO: a Curry-Howard approach to Church’s synthesis via linear logic. (English) Zbl 1453.03070

Proceedings of the 2018 33rd annual ACM/IEEE symposium on logic in computer science, LICS 2018, Oxford, UK, July 9–12, 2018. New York, NY: Association for Computing Machinery (ACM). 849-858 (2018).
PDF BibTeX XML Cite
Full Text: DOI

Differential equation axiomatization. The impressive power of differential ghosts. (English) Zbl 1453.03026

Proceedings of the 2018 33rd annual ACM/IEEE symposium on logic in computer science, LICS 2018, Oxford, UK, July 9–12, 2018. New York, NY: Association for Computing Machinery (ACM). 819-828 (2018).
PDF BibTeX XML Cite
Full Text: DOI arXiv

A proof theory for model checking: an extended abstract. (English) Zbl 1483.03034

Cervesato, Iliano (ed.) et al., Proceedings of the fourth international workshop on linearity, LINEARITY 2016, Porto, Portugal, June 25, 2016. Waterloo: Open Publishing Association (OPA). Electron. Proc. Theor. Comput. Sci. (EPTCS) 238, 1-10 (2017).
MSC:  03F52 68Q60
PDF BibTeX XML Cite
Full Text: arXiv Link

A proof system for MSVL programs in Coq. (English) Zbl 1461.68058

Liu, Shaoying (ed.) et al., Structured object-oriented formal language and method. 6th international workshop, SOFL+MSVL 2016, Tokyo, Japan, November 15, 2016. Revised selected papers. Cham: Springer. Lect. Notes Comput. Sci. 10189, 121-143 (2017).
PDF BibTeX XML Cite
Full Text: DOI

CSimpl: a rely-guarantee-based framework for verifying concurrent programs. (English) Zbl 1452.68053

Legay, Axel (ed.) et al., Tools and algorithms for the construction and analysis of systems. 23rd international conference, TACAS 2017, held as part of the European joint conferences on theory and practice of software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017. Proceedings. Part I. Berlin: Springer. Lect. Notes Comput. Sci. 10205, 481-498 (2017).
MSC:  68N30 68Q60 68Q85
PDF BibTeX XML Cite
Full Text: DOI Link

Dijkstra monads for free. (English) Zbl 1380.68266

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). 515-529 (2017).
MSC:  68Q60 68N30 68Q55 68T15
PDF BibTeX XML Cite
Full Text: DOI arXiv

Computer arithmetic and formal proofs. Verifying floating-point algorithms with the Coq system. (English) Zbl 1385.68001

Amsterdam: Elsevier/ISTE Press (ISBN 978-1-78548-112-3/hbk; 978-0-08-101170-6/ebook). xx, 306 p. (2017).
MSC:  68-02 65G50 65Y04 68Q60 68T15
PDF BibTeX XML Cite
Full Text: Link

Towards completeness via proof search in the linear time \(\mu\)-calculus: the case of Büchi inclusions. (English) Zbl 1401.68193

Proceedings of the 2016 31st annual ACM/IEEE symposium on logic in computer science, LICS 2016, New York City, NY, USA, July 5–8, 2016. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-4391-6). 377-386 (2016).
PDF BibTeX XML Cite
Full Text: DOI

Proof certificates for equality reasoning. (English) Zbl 1394.68350

Benevides, Mario (ed.) et al., Proceedings of the 10th workshop on logical and semantic frameworks, with applications (LSFA 2015), Natal, Brazil, August 31 – September 1, 2015. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 323, 93-108 (2016).
MSC:  68T15 03F07 68Q42
PDF BibTeX XML Cite
Full Text: DOI

Brief announcement: Space-time tradeoffs for distributed verification. (English) Zbl 1374.68270

Proceedings of the 2016 ACM symposium on principles of distributed computing, PODC ’16, Chicago, IL, USA, July 25–28, 2016. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-3964-3). 357-359 (2016).
PDF BibTeX XML Cite
Full Text: DOI arXiv

Saturation-based incremental LTL model checking with inductive proofs. (English) Zbl 1420.68135

Baier, Christel (ed.) et al., Tools and algorithms for the construction and analysis of systems. 21st international conference, TACAS 2015, held as part of the European joint conferences on theory and practice of software, ETAPS 2015, London, UK, April 11–18, 2015. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 9035, 643-657 (2015).
MSC:  68Q60 03B44 68Q85
PDF BibTeX XML Cite
Full Text: DOI Link

An LTL proof system for runtime verification. (English) Zbl 1420.68121

Baier, Christel (ed.) et al., Tools and algorithms for the construction and analysis of systems. 21st international conference, TACAS 2015, held as part of the European joint conferences on theory and practice of software, ETAPS 2015, London, UK, April 11–18, 2015. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 9035, 581-595 (2015).
MSC:  68Q60 03B44
PDF BibTeX XML Cite
Full Text: DOI Link

Proof spaces for unbounded parallelism. (English) Zbl 1345.68102

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). 407-420 (2015).
MSC:  68N30 68Q45 68Q60
PDF BibTeX XML Cite
Full Text: DOI Link

Proving concurrent constraint programming correct, revisited. (English) Zbl 1342.68238

Ayala-Rincón, Mauricio (ed.) et al., Proceedings of the 9th workshop on logical and semantic frameworks, with applications (LSFA 2014), Brasilia, Brazil, September 8–9, 2014. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 312, 179-195, electronic only (2015).
PDF BibTeX XML Cite
Full Text: DOI

Integrating simplex with tableaux. (English) Zbl 1471.68304

De Nivelle, Hans (ed.), Automated reasoning with analytic tableaux and related methods. 24th international conference, TABLEAUX 2015, Wrocław, Poland, September 21–24, 2015. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9323, 86-101 (2015).
MSC:  68V15 03B35
PDF BibTeX XML Cite
Full Text: DOI Link

Abstract interpretation: past, present and future. (English) Zbl 1401.68037

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. 2, 10 p. (2014).
MSC:  68N30 68Q60
PDF BibTeX XML Cite
Full Text: DOI

Mathematics and the new technologies. I: Philosophical relevance of a changing culture of mathematics. (English) Zbl 1368.00022

Schroeder-Heister, Peter (ed.) et al., Logic, methodology and philosophy of science. Logic and science facing the new technologies. Proceedings of the 14th international congress, Nancy, France, July 19–26, 2011. London: College Publications (ISBN 978-1-84890-169-8/pbk). 399-407 (2014).
MSC:  00A30
PDF BibTeX XML Cite

Lem: reusable engineering of real-world semantics. (English) Zbl 1346.68123

Proceedings of the 19th ACM SIGPLAN international conference on functional programming, ICFP ’14, Gothenburg, Sweden, September 1–3, 2014. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-2873-9). 175-188 (2014).
MSC:  68Q60 68Q55 68T15
PDF BibTeX XML Cite
Full Text: DOI

Modelling the usage of partial functions and undefined terms using presupposition theory. (English) Zbl 1344.03032

Geschke, Stefan (ed.) et al., Infinity, computability and metamathematics. Festschrift celebrating the 60th birthdays of Peter Koepke and Philip Welch. London: College Publications (ISBN 978-1-84890-130-8/hbk). 71-88 (2014).
MSC:  03B65 68T15 68T50
PDF BibTeX XML Cite

A pipelined multi-core MIPS machine. Hardware implementation and correctness proof. (English) Zbl 1304.68005

Lecture Notes in Computer Science 9000. Cham: Springer (ISBN 978-3-319-13905-0/pbk). xii, 352 p. (2014).
PDF BibTeX XML Cite
Full Text: DOI

A proof system for separation logic with magic wand. (English) Zbl 1284.68408

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). 477-490 (2014).
MSC:  68Q60 03B70 68T15
PDF BibTeX XML Cite
Full Text: DOI

30 years of research and development around Coq. (English) Zbl 1284.68517

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). 249-249 (2014).
MSC:  68T15 68-03 68N30 68Q60
PDF BibTeX XML Cite
Full Text: DOI

A constraint-based approach to solving games on infinite graphs. (English) Zbl 1284.91009

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). 221-233 (2014).
PDF BibTeX XML Cite
Full Text: DOI Link

Distributed verification using mobile agents. (English) Zbl 1351.68037

Frey, Davide (ed.) et al., Distributed computing and networking. 14th international conference, ICDCN 2013, Mumbai, India, January 3–6, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-35667-4/pbk). Lecture Notes in Computer Science 7730, 330-347 (2013).
MSC:  68M14 68Q60
PDF BibTeX XML Cite
Full Text: DOI

Checking proofs. (English) Zbl 1330.00021

Aberdein, Andrew (ed.) et al., The argument of mathematics. Dordrecht: Springer (ISBN 978-94-007-6533-7/hbk; 978-94-007-6534-4/ebook). Logic, Epistemology, and the Unity of Science 30, 147-170 (2013).
MSC:  00A30 00A35 03-03 01A60 01A61 03B35 68T15
PDF BibTeX XML Cite
Full Text: DOI

Type binding as a method of combining logics. (Russian. English summary) Zbl 1299.03005

Pinus, A. G. (ed.) et al., Algebra and model theory 9. Collection of papers from the 10th summer school “Frontiers in model theory and universal algebra”, Erlogol, Russia, June 25–29, 2013. Novosibirsk: Novosibirsk State Technical University (ISBN 978-5-7782-2350-9). 144-153 (2013).
MSC:  03B35 03B62 68T15 68T30
PDF BibTeX XML Cite

Zenon modulo: when Achilles outruns the tortoise using deduction modulo. (English) Zbl 1406.68105

McMillan, Ken (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 19th international conference, LPAR-19, Stellenbosch, South Africa, December 14–19, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-45220-8/pbk). Lecture Notes in Computer Science 8312, 274-290 (2013).
MSC:  68T15
PDF BibTeX XML Cite
Full Text: DOI Link

Linear time proof verification on N-graphs: a graph theoretic approach. (English) Zbl 1394.03018

Libkin, Leonid (ed.) et al., Logic, language, information, and computation. 20th international workshop, WoLLIC 2013, Darmstadt, Germany, August 20–23, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-39991-6/pbk). Lecture Notes in Computer Science 8071, 34-48 (2013).
MSC:  03B35 03F07
PDF BibTeX XML Cite
Full Text: DOI

Relating reasoning methodologies in linear logic and process algebra. (English) Zbl 1459.68139

Alves, Sandra (ed.) et al., Proceedings of the 2nd international workshop on linearity, Tallinn, Estonia, April 1, 2012. Waterloo: Open Publishing Association (OPA). Electron. Proc. Theor. Comput. Sci. (EPTCS) 101, 50-60 (2012).
MSC:  68Q85 03F52 68Q60
PDF BibTeX XML Cite
Full Text: arXiv Link

The complete proof theory of hybrid systems. (English) Zbl 1364.03045

Proceedings of the 2012 27th annual ACM/IEEE symposium on logic in computer science, LICS 2012, Dubrovnik, Croatia, June 25–28, 2012. Los Alamitos, CA: IEEE Computer Society (ISBN 978-0-7695-4769-5). 541-550 (2012).
PDF BibTeX XML Cite
Full Text: DOI

Freefinement. (English) Zbl 1321.68209

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

Analysis of methods for extraction of programs from non-constructive proofs. (English) Zbl 1252.68028

München: Univ. München, Fakultät für Mathematik, Informatik und Statistik (Diss.). xi, 167 p. (2012).
PDF BibTeX XML Cite
Full Text: Link

Tableaux modulo theories using superdeduction. An application to the verification of B proof rules with the Zenon automated theorem prover. (English) Zbl 1358.68255

Gramlich, Bernhard (ed.) et al., Automated reasoning. 6th international joint conference, IJCAR 2012, Manchester, UK, June 26–29, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-31364-6/pbk). Lecture Notes in Computer Science 7364. Lecture Notes in Artificial Intelligence, 332-338 (2012).
MSC:  68T15 03B35 68Q60
PDF BibTeX XML Cite
Full Text: DOI arXiv

Fast and compact self stabilizing verification, computation, and fault detection of an MST. (English) Zbl 1321.68348

Proceedings of the 30th annual ACM SIGACT-SIGOPS symposium on principles of distributed computing, PODC ’11, San Jose, CA, USA, June 06–08, 2011. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-0719-2). 311-320 (2011).
PDF BibTeX XML Cite
Full Text: DOI arXiv

Verified squared, does critical software deserve verified tools? (English) Zbl 1284.68189

Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’11, Austin, TX, USA, January 26–28, 2011. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-0490-0). 1-2 (2011).
MSC:  68N30 68Q60 68T15
PDF BibTeX XML Cite
Full Text: DOI

Filter Results by …

Document Type

Reviewing State

all top 5

Author

all top 5

Serial

all top 5

Year of Publication

all top 3

Classification

all top 3

Software