Search results for "theorem proving"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
3	Maria Paola Bonacina	On theorem proving for program checking: historical perspective and recent developments.	PPDP	2010	DBLP DOI BibTeX RDF	combination of theories, rewrite-based theorem proving, speculative inferences, satisfiability modulo theories
3	Yingying Jiang, Feng Tian, Hongan Wang, Xiaolong Zhang, XuGang Wang, Guozhong Dai	Intelligent understanding of handwritten geometry theorem proving.	IUI	2010	DBLP DOI BibTeX RDF	geometry theorem proving, hand-drawn figures, hand-written proof scripts, structure based manipulation, recognition
3	David R. Lester	Real Number Calculations and Theorem Proving.	TPHOLs	2008	DBLP DOI BibTeX RDF	Computable Reals, Exact Arithmetic, Theorem Proving, PVS, Higher-order Logic
3	Yuyan Chao, Lifeng He, Tsuyoshi Nakamura, Zhenghao Shi, Kenji Suzuki, Hidenori Itoh	An Improvement of Herbrand's Theorem and Its Application to Model Generation Theorem Proving.	J. Comput. Sci. Technol.	2007	DBLP DOI BibTeX RDF	Herbrand’s theorem, Herbrand universe, model generation theorem proving, SATCHMO, really non-propositinal
3	Sandip Ray, Rob Sumners	Combining Theorem Proving with Model Checking through Predicate Abstraction.	IEEE Design & Test of Computers	2007	DBLP DOI BibTeX RDF	model checking, formal verification, theorem proving, predicate abstraction, ACL2
3	Quan Liu, Yang Gao 0001, Zhiming Cui, WangShu Yao, ZhongWen Chen	An Tableau Automated Theorem Proving Method Using Logical Reinforcement Learning.	ISICA	2007	DBLP DOI BibTeX RDF	logical reinforcement learning, tableau automated theorem proving, LOMDP
3	Panagiotis Manolios, Daron Vroon	Integrating static analysis and general-purpose theorem proving for termination analysis.	ICSE	2006	DBLP DOI BibTeX RDF	static analysis, theorem proving, termination, liveness, ACL2
3	Youngsik Kim, Parija Sule, Nazanin Mansouri	Exploiting PSL standard assertions in a theorem-proving-based verification environment.	ACM Great Lakes Symposium on VLSI	2005	DBLP DOI BibTeX RDF	assertion-based design, modeling, verification, theorem-proving, formal semantics, PSL
3	Chiyan Chen, Hongwei Xi	Combining programming with theorem proving.	ICFP	2005	DBLP DOI BibTeX RDF	applied type system, proof erasure, theorem proving, dependent types, ATS
3	César Muñoz, David R. Lester	Real Number Calculations and Theorem Proving.	TPHOLs	2005	DBLP DOI BibTeX RDF
3	Wing-Kwong Wong, Bo-Yu Chan, Sheng-Kai Yin	A Dynamic Geometry Environment for Learning Theorem Proving.	ICALT	2005	DBLP DOI BibTeX RDF	learning geometry, geometry education, theorem proving, Dynamic geometry
3	Hai Lin 0005, Jigui Sun, Yimin Zhang	Theorem Proving Based on the Extension Rule.	J. Autom. Reasoning	2003	DBLP DOI BibTeX RDF	extension rule, inclusion-exclusion principle, complementary factor, theorem proving
3	Gilles Dowek, Thérèse Hardin, Claude Kirchner	Theorem Proving Modulo.	J. Autom. Reasoning	2003	DBLP DOI BibTeX RDF	sequent calculus modulo, resolution, rewriting, automated theorem proving, higher-order logic, cut elimination, narrowing, Skolemization, deduction modulo
3	Konrad Slind, Joe Hurd	Applications of Polytypism in Theorem Proving.	TPHOLs	2003	DBLP DOI BibTeX RDF
3	June Andronick, Boutheina Chetali, Olivier Ly	Using Coq to Verify Java Card Applet Isolation Properties.	TPHOLs	2003	DBLP DOI BibTeX RDF	Security, Theorem Proving, Smart Card
3	Miroslav Popovic, Vladimir Kovacevic, Ivan Velikic	A Formal Software Verification Concept Based on Automated Theorem Proving and Reverse Engineering. (PDF / PS)	ECBS	2002	DBLP DOI BibTeX RDF	formal software verification, fault-tolerant and robust software, mission-critical embedded software, reverse engineering, automated theorem proving, predicate calculus
3	Hongbo Li	Algebraic Representation, Elimination and Expansion in Automated Geometric Theorem Proving.	Automated Deduction in Geometry	2002	DBLP DOI BibTeX RDF	Cayley algebra, bracket algebra, affine geometry, automated theorem proving, projective geometry, conics
3	Simon Ambler, Roy L. Crole, Alberto Momigliano	Combining Higher Order Abstract Syntax with Tactical Theorem Proving and (Co)Induction.	TPHOLs	2002	DBLP DOI BibTeX RDF
3	Simon J. Gay	A Framework for the Formalisation of Pi Calculus Type Systems in Isabelle/HOL.	TPHOLs	2001	DBLP DOI BibTeX RDF	semantics, Types, pi calculus, automatic theorem proving
3	Fausto Giunchiglia, Paolo Traverso	Theorem proving in technology transfer: the user's point of view.	STTT	2000	DBLP DOI BibTeX RDF	Formal methods, Mechanized theorem proving
3	Harald Ganzinger, Viorica Sofronie-Stokkermans	Chaining Techniques for Automated Theorem Proving in Many-Valued Logics. (PDF / PS)	ISMVL	2000	DBLP DOI BibTeX RDF	chaining calculi, resolution, many-valued logic, automated theorem proving, superposition
3	Roope Kaivola, Mark Aagaard	Divider Circuit Verification with Model Checking and Theorem Proving.	TPHOLs	2000	DBLP DOI BibTeX RDF
3	Viorica Sofronie-Stokkermans	Representation Theorems and Theorem Proving in Non-Classical Logics. (PDF / PS)	ISMVL	1999	DBLP DOI BibTeX RDF	distributive lattices with operators, Priestley duality, many-values logics, automated theorem proving, Non-classical logics
3	Mark Aagaard, Robert B. Jones, Carl-Johan H. Seger	Lifted-FL: A Pragmatic Implementation of Combined Model Checking and Theorem Proving.	TPHOLs	1999	DBLP DOI BibTeX RDF
3	François Puitg, Jean-François Dufourd	Formal Specification and Theorem Proving Breakthroughs in Geometric Modeling.	TPHOLs	1998	DBLP DOI BibTeX RDF
3	Naren Narasimhan, Ranga Vemuri	On the Effectiveness of Theorem Proving Guided Discovery of Formal Assertions for a Register Allocator in a High-Level Synthesis System.	TPHOLs	1998	DBLP DOI BibTeX RDF
3	Adel Bouhoula, Jean-Pierre Jouannaud	Automata-Driven Automated Induction.	LICS	1997	DBLP DOI BibTeX RDF	automata-driven automated induction, inductive theorem proving, first-order functions, finitely many unary membership predicates, rational subsets, ground reducibility, inductive prover, theorem proving, tree automata, Horn Clauses, proof obligations
3	Chih-Hung Wu, Shie-Jue Lee	On parallelism of hyper-linking theorem proving: a preliminary report. (PDF / PS)	ICPADS	1996	DBLP DOI BibTeX RDF	hyper-linking theorem proving, hyper-linking proof procedure, phase-level, clause-level, literal-level, search level parallelism, parallel strategies, parallel algorithms, parallelism, artificial intelligence, parallel architectures, theorem proving
3	Miriam Leeser, John W. O'Leary	Verification of a subtractive radix-2 square root algorithm and implementation. (PDF / PS)	ICCD	1995	DBLP DOI BibTeX RDF	subtractive radix-2 square root, floating point square root hardware, Intel Pentium, radix-2 square root, MIPS R4400, RTL level, verification, formal verification, theorem proving, theorem proving, floating point arithmetic, optimizing transformations
3	Sreeranga P. Rajan, Jeffrey J. Joyce, Carl-Johan H. Seger	From Abstract Data Types to Shift Registers: A Case Study in Formal Specification and Verification at Differing Levels of Abstraction using Theorem Proving and Symbolic Simulation.	HUG	1993	DBLP DOI BibTeX RDF
3	Ming-Yi Fang, Wen-Tsuen Chen	Vectorization of a Generalized Procedure for Theorem Proving in Propositional Logic on Vector Computers.	IEEE Trans. Knowl. Data Eng.	1992	DBLP DOI BibTeX RDF	artificial intelligence, theorem proving, theorem proving, formal logic, propositional logic, vector processor systems, vectorisation, vector computers, deduction rules
3	Robert E. Fields, Morten Elvang-Gøransson	A VDM Case Study in mural.	IEEE Trans. Software Eng.	1992	DBLP DOI BibTeX RDF	interactive theorem-proving assistant, specification support tool, mural, verification, formal specification, specification, software tools, theorem proving, program verification, interactive systems, VDM, Vienna development method
3	Zohar Manna, Richard J. Waldinger	Fundamentals of Deductive Program Synthesis.	IEEE Trans. Software Eng.	1992	DBLP DOI BibTeX RDF	deductive program synthesis, deductive-tableau system, theorem-proving framework, nonclausal resolution rule, induction rule, formal specification, artificial intelligence, specification, theorem proving, program testing, reasoning, inference mechanisms, proof
3	Sun Yong-qiang, Lu Ru-zhan, Bi Hua	Program synthesis based on Boyer-Moore theorem proving techniques.	ACM Conference on Computer Science	1985	DBLP DOI BibTeX RDF	Boyer-Moore technique, program sysnthesis, theorem proving, resolution
2	Phil Scott, Jacques D. Fleuriot	Composable Discovery Engines for Interactive Theorem Proving.	ITP	2011	DBLP DOI BibTeX RDF
2	Osman Hasan, Sofiène Tahar, Naeem Abbasi	Formal Reliability Analysis Using Theorem Proving.	IEEE Trans. Computers	2010	DBLP DOI BibTeX RDF	theorem proving, Formal models, memory structures, performance and reliability
2	David C. J. Matthews, Makarius Wenzel	Efficient parallel programming in Poly/ML and Isabelle/ML.	DAMP	2010	DBLP DOI BibTeX RDF	parallel standard ml, poly/ml, theorem proving applications, data parallelism, isabelle
2	Geoff Sutcliffe, Christoph Benzmüller, Chad E. Brown, Frank Theiss	Progress in the Development of Automated Theorem Proving for Higher-Order Logic.	CADE	2009	DBLP DOI BibTeX RDF
2	Stephan Swiderski, Michael Parting, Jürgen Giesl, Carsten Fuhs, Peter Schneider-Kamp	Termination Analysis by Dependency Pairs and Inductive Theorem Proving.	CADE	2009	DBLP DOI BibTeX RDF
2	Martin Suda, Geoff Sutcliffe, Patrick Wischnewski, Manuel Lamotte-Schubert, Gerard de Melo	External Sources of Axioms in Automated Theorem Proving.	KI	2009	DBLP DOI BibTeX RDF
2	Anduo Wang, Prithwish Basu, Boon Thau Loo, Oleg Sokolsky	Declarative Network Verification.	PADL	2009	DBLP DOI BibTeX RDF	network protocol verification, theorem proving, domain-specific languages, Declarative networking
2	David Déharbe, Silvio Ranise	Satisfiability solving for software verification.	STTT	2009	DBLP DOI BibTeX RDF	Equational theorem proving, Boolean solving, Theory reasoning, Software verification
2	Karl-Heinz Pennemann	Resolution-Like Theorem Proving for High-Level Conditions.	ICGT	2008	DBLP DOI BibTeX RDF	first-order tautology problem, high-level conditions, weak adhesive HLR categories, theorem proving, resolution
2	Camilo Rocha, José Meseguer	Theorem Proving Modulo Based on Boolean Equational Procedures.	RelMiCS	2008	DBLP DOI BibTeX RDF
2	Mike Gordon	Twenty Years of Theorem Proving for HOLs Past, Present and Future.	TPHOLs	2008	DBLP DOI BibTeX RDF
2	Konstantine Arkoudas, Olin Shivers	Trusted Theorem Proving: A Case Study in SLD-Resolution.	ISoLA	2008	DBLP DOI BibTeX RDF
2	Russell O'Connor	Certified Exact Transcendental Real Number Computation in Coq.	TPHOLs	2008	DBLP DOI BibTeX RDF
2	Yves Bertot	A Short Presentation of Coq.	TPHOLs	2008	DBLP DOI BibTeX RDF
2	Makarius Wenzel, Lawrence C. Paulson, Tobias Nipkow	The Isabelle Framework.	TPHOLs	2008	DBLP DOI BibTeX RDF
2	Steven P. Miller	Will This Be Formal?	TPHOLs	2008	DBLP DOI BibTeX RDF	model checking, Formal methods, theorem proving, avionics
2	Youngsik Kim, Nazanin Mansouri	Automated formal verification of scheduling with speculative code motions.	ACM Great Lakes Symposium on VLSI	2008	DBLP DOI BibTeX RDF	formal verification, high level synthesis, automated theorem-proving, speculation
2	Yves Bertot, Vladimir Komendantsky	Fixed point semantics and partial recursion in Coq.	PPDP	2008	DBLP DOI BibTeX RDF	least fixed point semantics, non-terminating functions, program extraction, the Knaster-Tarski theorem, automated theorem proving
2	Tertia Hörne, John A. van der Poll	Planning as model checking: the performance of ProB vs NuSMV.	SAICSIT Conf.	2008	DBLP DOI BibTeX RDF	tableaux theorem proving, model checking, planning, satisfiability, BDDs, constraint logic programming
2	Christoph Sprenger, David A. Basin	Cryptographically-Sound Protocol-Model Abstractions.	CSF	2008	DBLP DOI BibTeX RDF	cryptographic soundness, formal methods, theorem proving, Cryptographic protocols, simulatability
2	Achim D. Brucker, Burkhart Wolff	HOL-OCL: A Formal Proof Environment for UML/OCL.	FASE	2008	DBLP DOI BibTeX RDF	holocl, ocl, Formal Method, Theorem Proving, uml
2	Andriy Dunets, Gerhard Schellhorn, Wolfgang Reif	Bounded Relational Analysis of Free Data Types.	TAP	2008	DBLP DOI BibTeX RDF	SAT checking, model checking, verification, formal methods, theorem proving, First-order logic, abstract data types
2	Julien Schmaltz, Dominique Borrione	A functional formalization of on chip communications.	Formal Asp. Comput.	2008	DBLP DOI BibTeX RDF	Formal methods, Networks on chip, Automated theorem proving, Communication architectures
2	Volker Sorge, Andreas Meier, Roy L. McCasland, Simon Colton	Automatic Construction and Verification of Isotopy Invariants.	J. Autom. Reasoning	2008	DBLP DOI BibTeX RDF	Automated mathematics, Classification theorems, Computer algebra, Automated theorem proving, Model generation, SAT solving, Invariant generation, Isotopy
2	Viorica Sofronie-Stokkermans	Automated theorem proving by resolution in non-classical logics.	Ann. Math. Artif. Intell.	2007	DBLP DOI BibTeX RDF	Mathematics Subject Classifications (2000) 06D(05, 25,30,35,50), 03G(10,20)
2	Ashish Tiwari, Sumit Gulwani	Logical Interpretation: Static Program Analysis Using Theorem Proving.	CADE	2007	DBLP DOI BibTeX RDF
2	Shuaiqiang Wang, Jiancheng Wan, Jinkui Hou	OR-ATP: An Operation Refinement Approach As a Process of Automatic Theorem Proving.	SNPD	2007	DBLP DOI BibTeX RDF
2	Lawrence C. Paulson, Kong Woei Susanto	Source-Level Proof Reconstruction for Interactive Theorem Proving.	TPHOLs	2007	DBLP DOI BibTeX RDF
2	James Reynolds	Automatically Translating Type and Function Definitions from HOL to ACL2.	TPHOLs	2007	DBLP DOI BibTeX RDF
2	Lukas Bulwahn, Alexander Krauss, Tobias Nipkow	Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL.	TPHOLs	2007	DBLP DOI BibTeX RDF
2	Matthew Might	Logic-flow analysis of higher-order programs.	POPL	2007	DBLP DOI BibTeX RDF	LFA, abstract counting, abstract garbage collection, environment analysis, gamma-CFA first-order logic, logic-flow analysis, static analysis, theorem proving, lambda calculus, CPS
2	Fadoua Ghourabi, Tetsuo Ida, Hidekazu Takahashi, Mircea Marin, Asem Kasem	Logical and algebraic view of Huzita's origami axioms with applications to computational origami.	SAC	2007	DBLP DOI BibTeX RDF	constraint solving, first-order predicate logic, origami, geometric theorem proving
2	Osman Hasan, Sofiène Tahar	Verification of Probabilistic Properties in HOL Using the Cumulative Distribution Function.	IFM	2007	DBLP DOI BibTeX RDF	Higher-Order-Logic, Interactive Theorem Proving, HOL, Probabilistic Systems, Cumulative Distribution Function
2	Qiang Guan, Long Wang, Bican Xia, Lu Yang, Wensheng Yu, Zhenbing Zeng	Solution to the Generalized Champagne Problem on simultaneous stabilization of linear systems.	Science in China Series F: Information Sciences	2007	DBLP DOI BibTeX RDF	simultaneous stabilization, Champagne Problem, Generalized Champagne Problem, inequality-type theorem, stabilization, linear systems, automated theorem proving, complex analysis
2	David A. Basin, Hironobu Kuruma, Kunihiko Miyazaki, Kazuo Takaragi, Burkhart Wolff	Verifying a signature architecture: a comparative case study.	Formal Asp. Comput.	2007	DBLP DOI BibTeX RDF	Security, Model checking, Formal methods, Theorem proving, Case study, Comparison
2	Konrad Slind, Scott Owens, Juliano Iyoda, Mike Gordon	Proof producing synthesis of arithmetic and cryptographic hardware.	Formal Asp. Comput.	2007	DBLP DOI BibTeX RDF	Cryptography, Compiling, Theorem proving, Hardware synthesis, High assurance
2	Greta Yorsh, Thomas Ball, Mooly Sagiv	Testing, abstraction, theorem proving: better together!	ISSTA	2006	DBLP DOI BibTeX RDF	fabricated states, state-based coverage, testing, abstraction, program analysis, abstract interpretation, coverage, theorem prover, software fault injection, adequacy criteria
2	Eugenio Roanes-Macías, Eugenio Roanes-Lozano	A Maple Package for Automatic Theorem Proving and Discovery in 3D-Geometry.	Automated Deduction in Geometry	2006	DBLP DOI BibTeX RDF
2	Panagiotis Manolios	Refinement and Theorem Proving.	SFM	2006	DBLP DOI BibTeX RDF
2	Devrim Unal, M. Ufuk Çaglayan	Theorem proving for modeling and conflict checking of authorization policies.	ISCN	2006	DBLP DOI BibTeX RDF
2	Jim Woodcock, Leo Freitas	Z/Eves and the Mondex Electronic Purse.	ICTAC	2006	DBLP DOI BibTeX RDF	electronic finance, software archaeology, the Z notation, Z/Eves, security, refinement, theorem proving, smart cards, Grand Challenge, Verified Software Repository, Mondex
2	Xia Wu, Jigui Sun, Shuai Lu, Ying Li, Wei Meng, Minghao Yin	Improved Propositional Extension Rule.	RSKT	2006	DBLP DOI BibTeX RDF	Extension rule, reduced rule, theorem proving, propositional logic
2	Leo Freitas, Jim Woodcock, Ana Cavalcanti	State-rich model checking.	ISSE	2006	DBLP DOI BibTeX RDF	Formal method tools, Model checking, Theorem proving, Abstract interpretation
2	Sven Beyer, Christian Jacobi 0002, Daniel Kröning, Dirk Leinenbach, Wolfgang J. Paul	Putting it all together - Formal verification of the VAMP.	STTT	2006	DBLP DOI BibTeX RDF	Complete microprocessor verification, Tomasulo scheduler, Cache memory interface, Model checking, Formal methods, Theorem proving, Floating point unit
2	J. Strother Moore	Inductive assertions and operational semantics.	STTT	2006	DBLP DOI BibTeX RDF	Theorem proving, JVM, Software verification, Verification condition
2	Weiqiang Kong, Takahiro Seino, Kokichi Futatsugi, Kazuhiro Ogata	A Lightweight Integration of Theorem Proving and Model Checking for System Verification.	APSEC	2005	DBLP DOI BibTeX RDF
2	Yves Bertot, Laurent Théry	Dependent Types, Theorem Proving, and Applications for a Verifying Compiler.	VSTTE	2005	DBLP DOI BibTeX RDF
2	Sa Cui, Kevin Donnelly, Hongwei Xi	ATS: A Language That Combines Programming with Theorem Proving.	FroCos	2005	DBLP DOI BibTeX RDF
2	Christoph Benzmüller, Andreas Meier, Volker Sorge	Bridging Theorem Proving and Mathematical Knowledge Retrieval.	Mechanizing Mathematical Reasoning	2005	DBLP DOI BibTeX RDF
2	Steven Obua	Proving Bounds for Real Linear Programs in Isabelle/HOL.	TPHOLs	2005	DBLP DOI BibTeX RDF
2	Alma L. Juarez Dominguez, Nancy A. Day	Compositional reasoning for port-based distributed systems.	ASE	2005	DBLP DOI BibTeX RDF	DFC, model checking, theorem proving, compositional verification
2	Achim D. Brucker, Burkhart Wolff	Interactive Testing with HOL-TestGen.	FATES	2005	DBLP DOI BibTeX RDF	symbolic test case generations, theorem proving, black box testing, white box testing, interactive testing
2	June Andronick, Boutheina Chetali, Christine Paulin-Mohring	Formal Verification of Security Properties of Smart Card Embedded Source Code.	FM	2005	DBLP DOI BibTeX RDF	Source code verification, Security, Formal Methods, Theorem Proving, Smart Card
2	David Cachera, Thomas P. Jensen, David Pichardie, Gerardo Schneider	Certified Memory Usage Analysis.	FM	2005	DBLP DOI BibTeX RDF	certified memory analysis, Program analysis, theorem proving, constraint solving
2	Rajesh Kumar 0005, Bruce H. Krogh, Peter H. Feiler	An Ontology-Based Approach to Heterogeneous Verification of Embedded Control Systems.	HSCC	2005	DBLP DOI BibTeX RDF	ontology, theorem proving, knowledge base, knowledge integration
2	Alexander Koller, Ralph Debusmann, Malte Gabsdil, Kristina Striegnitz	Put My Galakmid Coin into the Dispenser and Kick It: Computational Linguistics and Theorem Proving in a Computer Game.	Journal of Logic, Language and Information	2004	DBLP DOI BibTeX RDF	text adventures, generation, description logic, parsing, theorem provers, reference resolution, dependency grammar
2	Maxim Makatchev, Pamela W. Jordan, Kurt VanLehn	Abductive Theorem Proving for Analyzing Student Explanations to Guide Feedback in Intelligent Tutoring Systems.	J. Autom. Reasoning	2004	DBLP DOI BibTeX RDF	intelligent tutoring systems, abductive reasoning, qualitative physics
2	Ghiath Al Sammane, Julien Schmaltz, Diana Toma, Pierre Ostier, Dominique Borrione	TheoSim: combining symbolic simulation and theorem proving for hardware verification.	SBCCI	2004	DBLP DOI BibTeX RDF	theorem proving, symbolic simulation, hardware verification
2	Alexander V. Lyaletski, Andrey Paskevich, Konstantin Verchinine	Theorem Proving and Proof Verification in the System SAD.	MKM	2004	DBLP DOI BibTeX RDF
2	Thomas F. Melham	Integrating Model Checking and Theorem Proving in a Reflective Functional Language.	IFM	2004	DBLP DOI BibTeX RDF
2	Arjen Hommersom, Peter J. F. Lucas, Michael Balser	Meta-level Verification of the Quality of Medical Guidelines Using Interactive Theorem Proving.	JELIA	2004	DBLP DOI BibTeX RDF
2	Fredrik Lindblad, Marcin Benke	A Tool for Automated Theorem Proving in Agda.	TYPES	2004	DBLP DOI BibTeX RDF
2	Behzad Akbarpour, Sofiène Tahar	Error Analysis of Digital Filters Using Theorem Proving.	TPHOLs	2004	DBLP DOI BibTeX RDF
2	Tomás Recio, Francisco Botana	Where the Truth Lies (in Automatic Theorem Proving in Elementary Geometry).	ICCSA	2004	DBLP DOI BibTeX RDF
2	Harald Ganzinger, Konstantin Korovin	Integrating Equational Reasoning into Instantiation-Based Theorem Proving.	CSL	2004	DBLP DOI BibTeX RDF
2	Tjark Weber	Towards Mechanized Program Verification with Separation Logic.	CSL	2004	DBLP DOI BibTeX RDF	Separation Logic, Interactive Theorem Proving, Formal Program Verification