000 04877nam a22006015i 4500
001 978-3-319-08970-6
003 DE-He213
005 20200421112234.0
007 cr nn 008mamaa
008 140628s2014 gw | s |||| 0|eng d
020 _a9783319089706
_9978-3-319-08970-6
024 7 _a10.1007/978-3-319-08970-6
_2doi
050 4 _aQA8.9-QA10.3
072 7 _aUYA
_2bicssc
072 7 _aMAT018000
_2bisacsh
072 7 _aCOM051010
_2bisacsh
082 0 4 _a005.131
_223
245 1 0 _aInteractive Theorem Proving
_h[electronic resource] :
_b5th International Conference, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings /
_cedited by Gerwin Klein, Ruben Gamboa.
264 1 _aCham :
_bSpringer International Publishing :
_bImprint: Springer,
_c2014.
300 _aXXII, 555 p. 90 illus.
_bonline resource.
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
347 _atext file
_bPDF
_2rda
490 1 _aLecture Notes in Computer Science,
_x0302-9743 ;
_v8558
505 0 _aMicrocode Verification - Another Piece of the Microprocessor Verification Puzzle -- Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK -- Towards a Formally Verified Proof Assistant -- Implicational Rewriting Tactics in HOL -- A Heuristic Prover for Real Inequalities -- A Formal Library for Elliptic Curves in the Coq Proof Assistant -- Truly Modular (Co) data types for Isabelle/HOL -- Cardinals in Isabelle/HOL -- Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code -- Showing Invariance Compositionally for a Process Algebra for Network Protocols -- A Computer-Algebra-Based Formal Proof of the Irrationality of (Si(B(3) -- From Operational Models to Information Theory; Side Channels in pGCL with Isabelle -- A Coq Formalization of Finitely Presented Modules -- Formalized, Effective Domain Theory in Coq -- Completeness and Decidability Results for CTL in Coq -- Hypermap Specification and Certified Linked Implementation Using Orbits -- A Verified Generate-Test-Aggregate Coq Library for Parallel Programs Extraction -- Experience Implementing a Performant Category-Theory Library in Coq -- A New and Formalized Proof of Abstract Completion -- HOL with Definitions: Semantics, Soundness and a Verified Implementation -- Verified Efficient Implementation of Gabow's Strongly Connected Component Algorithm -- Recursive Functions on Lazy Lists via Domains and Topologies -- Formal Verification of Optical Quantum Flip Gate -- Compositional Computational Reflection -- An Isabelle Proof Method Language -- Proof Pearl: Proving a Simple Von Neumann Machine Turing Complete -- The Reflective Milawa Theorem Prover Is Sound (Down to the Machine Code That Runs It) -- Balancing Lists: A Proof Pearl -- Unified Decision Procedures for Regular Expression Equivalence -- Collaborative Interactive Theorem Proving with Clide -- On the Formalization of Z-Transform in HOL -- Universe Polymorphism in Coq -- Asynchronous User Interaction and Tool Integration in Isabelle/PIDE -- HOL Constant Definition Done Right -- Rough Diamond: An Extension of Equivalence-Based Rewriting -- Formal C Semantics: Comp Cert and the C Standard -- Mechanical Certification of Loop Pipelining Transformations: A Preview.
520 _aThis book constitutes the proceedings of the 5th International Conference on Interactive Theorem Proving, ITP 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, in Vienna, Austria, in July 2014. The 35 papers presented in this volume were carefully reviewed and selected from 59 submissions. The topics range from theoretical foundations to implementation aspects and applications in program verification, security and formalization of mathematics.
650 0 _aComputer science.
650 0 _aSoftware engineering.
650 0 _aComputer security.
650 0 _aAlgorithms.
650 0 _aComputer logic.
650 0 _aMathematical logic.
650 0 _aArtificial intelligence.
650 1 4 _aComputer Science.
650 2 4 _aMathematical Logic and Formal Languages.
650 2 4 _aArtificial Intelligence (incl. Robotics).
650 2 4 _aLogics and Meanings of Programs.
650 2 4 _aSoftware Engineering.
650 2 4 _aSystems and Data Security.
650 2 4 _aAlgorithm Analysis and Problem Complexity.
700 1 _aKlein, Gerwin.
_eeditor.
700 1 _aGamboa, Ruben.
_eeditor.
710 2 _aSpringerLink (Online service)
773 0 _tSpringer eBooks
776 0 8 _iPrinted edition:
_z9783319089690
830 0 _aLecture Notes in Computer Science,
_x0302-9743 ;
_v8558
856 4 0 _uhttp://dx.doi.org/10.1007/978-3-319-08970-6
912 _aZDB-2-SCS
912 _aZDB-2-LNC
942 _cEBK
999 _c58166
_d58166