Search results for "re-proving"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
52	Zohar Manna, Stephen Nes, Jean Vuillemin	Inductive methods for proving properties of programs.	Proving Assertions About Programs	1972	DBLP DOI BibTeX RDF
47	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
44	Tsong Yueh Chen, T. H. Tse, Zhiquan Zhou	Semi-proving: an integrated method based on global symbolic evaluation and metamorphic testing.	ISSTA	2002	DBLP DOI BibTeX RDF	global symbolic evaluation, program proving, semi-proving, program testing, symbolic execution, metamorphic testing
42	Sandip Ray, Rob Sumners	Combining Theorem Proving with Model Checking through Predicate Abstraction.	IEEE Des. Test Comput.	2007	DBLP DOI BibTeX RDF	model checking, formal verification, theorem proving, predicate abstraction, ACL2
42	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
42	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
41		Proceedings of ACM Conference on Proving Assertions About Programs, Las Cruces, New Mexico, USA, January 6-7, 1972	Proving Assertions About Programs	1972	DBLP DOI BibTeX RDF
41	Michel Sintzoff	Calculating properties of programs by valuations on specific models.	Proving Assertions About Programs	1972	DBLP DOI BibTeX RDF
41	Cliff B. Jones	Formal development of correct algorithms: An example based on earley's recogniser.	Proving Assertions About Programs	1972	DBLP DOI BibTeX RDF
41	Robin Milner	Implementation and applications of Scott's logic for computable functions.	Proving Assertions About Programs	1972	DBLP DOI BibTeX RDF
41	Clement L. McGowan	The "most recent" error: Its causes and correction.	Proving Assertions About Programs	1972	DBLP DOI BibTeX RDF
41	Peter Wegner	Operational semantics of programming languages.	Proving Assertions About Programs	1972	DBLP DOI BibTeX RDF
41	Clement McGowan	The Contour Model Lambda Calculus Machine.	Proving Assertions About Programs	1972	DBLP DOI BibTeX RDF
41	Daniel M. Berry	The equivalence of models of tasking.	Proving Assertions About Programs	1972	DBLP DOI BibTeX RDF
41	Jean-Marie Cadiou, Zohar Manna	Recursive definitions of partial functions and their computations.	Proving Assertions About Programs	1972	DBLP DOI BibTeX RDF
41	Michael J. Fischer	Lambda calculus schemata.	Proving Assertions About Programs	1972	DBLP DOI BibTeX RDF
41	Stephen J. Garland, David C. Luckham	Translating recursion schemes into program schemes.	Proving Assertions About Programs	1972	DBLP DOI BibTeX RDF
41	John A. N. Lee	The definition and validation of the radix sorting technique.	Proving Assertions About Programs	1972	DBLP DOI BibTeX RDF
41	C. David Allen	Derivation of axiomatic definitions of programming languages from algorithmic definitions.	Proving Assertions About Programs	1972	DBLP DOI BibTeX RDF
41	Edward A. Ashcroft	Program correctness methods and language definition.	Proving Assertions About Programs	1972	DBLP DOI BibTeX RDF
41	Michael S. Paterson	Decision problems in computational models.	Proving Assertions About Programs	1972	DBLP DOI BibTeX RDF
41	Raymond E. Miller	A boundary between decidability and undecidability for parallel program schemata (Extended Abstract).	Proving Assertions About Programs	1972	DBLP DOI BibTeX RDF
41	Thomas E. Hull, Wayne H. Enright, Arthur E. Sedgwick	The correctness of numerical algorithms.	Proving Assertions About Programs	1972	DBLP DOI BibTeX RDF
41	Ralph L. London	Correctness of a compiler for a Lisp subset.	Proving Assertions About Programs	1972	DBLP DOI BibTeX RDF
41	Thomas E. Cheatham Jr., Ben Wegbreit	On a laboratory for the study of automating programming.	Proving Assertions About Programs	1972	DBLP DOI BibTeX RDF
41	H. Raymond Strong, S. A. Walker	Properties preserved under recursion removal.	Proving Assertions About Programs	1972	DBLP DOI BibTeX RDF
41	Rod M. Burstall	An algebraic description of programs with assertions, verification and simulation.	Proving Assertions About Programs	1972	DBLP DOI BibTeX RDF
39	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
37	Su Feng	Mechanizing Weakly Ground Termination Proving of Term Rewriting Systems by Structural and Cover-Set Inductions.	J. Comput. Sci. Technol.	2005	DBLP DOI BibTeX RDF	automated formal proving, cover-set induction, dynamic term rewriting calculus, weakly ground termination, term rewriting system
37	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
37	Hongbo Li 0012	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
37	Miroslav Popovic, Vladimir Kovacevic, Ivan Velikic	A Formal Software Verification Concept Based on Automated Theorem Proving and Reverse Engineering.	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
37	Fausto Giunchiglia, Paolo Traverso	Theorem proving in technology transfer: the user's point of view.	Int. J. Softw. Tools Technol. Transf.	2000	DBLP DOI BibTeX RDF	Formal methods, Mechanized theorem proving
37	Mark D. 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
37	Anna Mikhajlova, Joakim von Wright	Proving Isomorphism of First-Order Logic Proof Systems in HOL.	TPHOLs	1998	DBLP DOI BibTeX RDF
37	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
35	Benny Godlin, Ofer Strichman	Inference rules for proving the equivalence of recursive procedures.	Acta Informatica	2008	DBLP DOI BibTeX RDF
35	Paul A. Cairns, Jeremy Gow	Literate Proving: Presenting and Documenting Formal Proofs.	MKM	2005	DBLP DOI BibTeX RDF
35	Maria Paola Bonacina, Jieh Hsiang	On Fairness of Completion-Based Theorem Proving Strategies.	RTA	1991	DBLP DOI BibTeX RDF
35	Larry Wos	Solving Open Questions with an Automated Theorem-Proving Program.	CADE	1982	DBLP DOI BibTeX RDF
35	Chih-Hung Wu, Shie-Jue Lee	On parallelism of hyper-linking theorem proving: a preliminary report.	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
35	Miguel Felder, Dino Mandrioli, Angelo Morzenti	Proving Properties of Real-Time Systems Through Logical Specifications and Petri Net Models.	IEEE Trans. Software Eng.	1994	DBLP DOI BibTeX RDF	property proving, logical specifications, TRIO, Hoare method, dual language, real-time systems, real-time systems, embedded systems, formal specification, formal specification, Petri nets, temporal logic, temporal logic, theorem proving, first-order logic, timed Petri net, formal analysis, axiomatization
35	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
33	Yingying Jiang 0001, Feng Tian 0001, Hongan Wang, Xiaolong Zhang 0001, 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
33	Hai Lin 0008, Jigui Sun, Yimin Zhang 0005	Theorem Proving Based on the Extension Rule.	J. Autom. Reason.	2003	DBLP DOI BibTeX RDF	extension rule, inclusion-exclusion principle, complementary factor, theorem proving
33	Gilles Dowek, Thérèse Hardin, Claude Kirchner	Theorem Proving Modulo.	J. Autom. Reason.	2003	DBLP DOI BibTeX RDF	sequent calculus modulo, resolution, rewriting, automated theorem proving, higher-order logic, cut elimination, narrowing, Skolemization, deduction modulo
33	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
32	Vlad Rusu, Eli Singerman	On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction.	TACAS	1999	DBLP DOI BibTeX RDF
32	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
32	I. S. W. B. Prasetya	On the Style of Mechanical Proving.	HUG	1993	DBLP DOI BibTeX RDF
31	David A. Basin, Hironobu Kuruma, Kunihiko Miyazaki, Kazuo Takaragi, Burkhart Wolff	Verifying a signature architecture: a comparative case study.	Formal Aspects Comput.	2007	DBLP DOI BibTeX RDF	Security, Model checking, Formal methods, Theorem proving, Case study, Comparison
31	David A. Plaisted	Special Cases and Substitutes for Rigid E-Unification.	Appl. Algebra Eng. Commun. Comput.	2000	DBLP DOI BibTeX RDF	Rigid E -unification, Theorem proving, First-order logic, Decidability, Unification, Equality, Horn clauses, Tableaux
31	Weiqiang Kong, Takahiro Seino, Kokichi Futatsugi, Kazuhiro Ogata 0001	A Lightweight Integration of Theorem Proving and Model Checking for System Verification.	APSEC	2005	DBLP DOI BibTeX RDF
31	Christoph Benzmüller, Andreas Meier 0002, Volker Sorge	Bridging Theorem Proving and Mathematical Knowledge Retrieval.	Mechanizing Mathematical Reasoning	2005	DBLP DOI BibTeX RDF
31	Helko Lehmann, Michael Leuschel	Inductive Theorem Proving by Program Specialisation: Generating Proofs for Isabelle Using Ecce.	LOPSTR	2003	DBLP DOI BibTeX RDF
31	Marta Franová	Automated Inductive Reasoning as a Support of Deductive Reasoning in a User-Independent Automation of Inductive Theorem Proving.	ISMIS	1996	DBLP DOI BibTeX RDF
31	Jieh Hsiang, Mandayam K. Srivas	PROLOG-Based Inductive Theorem Proving.	FSTTCS	1985	DBLP DOI BibTeX RDF
29	Ueli M. Maurer	Unifying Zero-Knowledge Proofs of Knowledge.	AFRICACRYPT	2009	DBLP DOI BibTeX RDF
28	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
28	Miriam Leeser, John W. O'Leary	Verification of a subtractive radix-2 square root algorithm and implementation.	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
28	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
28	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
28	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
28	Wolfgang Schreiner	The RISC ProofNavigator: a proving assistant for program verification in the classroom.	Formal Aspects Comput.	2009	DBLP DOI BibTeX RDF	Interactive proving assistants, Teaching formal methods, Computer-aided verification
28	Yuyan Chao, Lifeng He, Tsuyoshi Nakamura, Zhenghao Shi, Kenji Suzuki 0001, 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
28	Panagiotis Manolios, Daron Vroon 0001	Integrating static analysis and general-purpose theorem proving for termination analysis.	ICSE	2006	DBLP DOI BibTeX RDF	static analysis, theorem proving, termination, liveness, ACL2
28	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
28	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
28	Stefan Blom, Jaco van de Pol	State Space Reduction by Proving Confluence.	CAV	2002	DBLP DOI BibTeX RDF	on-the-fly state space reduction, symbolic transformation, &#55CRL tool set, theorem proving, Labeled transition systems, partial order reduction, confluence, branching bisimulation
28	Andrei Voronkov	How to optimize proof-search in modal logics: new methods of proving redundancy criteria for sequent calculi.	ACM Trans. Comput. Log.	2001	DBLP DOI BibTeX RDF	theorem proving, modal logic, description logics, proof-search, inverse method
28	Harald Ganzinger, Viorica Sofronie-Stokkermans	Chaining Techniques for Automated Theorem Proving in Many-Valued Logics.	ISMVL	2000	DBLP DOI BibTeX RDF	chaining calculi, resolution, many-valued logic, automated theorem proving, superposition
28	Viorica Sofronie-Stokkermans	Representation Theorems and Theorem Proving in Non-Classical Logics.	ISMVL	1999	DBLP DOI BibTeX RDF	distributive lattices with operators, Priestley duality, many-values logics, automated theorem proving, Non-classical logics
28	Oliver Bittel	Tableau-Based Theorem Proving and Synthesis of Lambda-Terms in the Intuitionistic Logic.	JELIA	1992	DBLP DOI BibTeX RDF	Typed -Calculus, Program Synthesis, Intuitionistic Logic, Automatic Theorem Proving
28	Donald I. Good, Richard M. Cohen, James G. Keeton-Williams	Principles of Proving Programs Correct in Gypsy.	POPL	1979	DBLP DOI BibTeX RDF	message buffers, program proving, formal specifications, parallel programs, concurrency, program verification
27	Laurent Théry, Guillaume Hanrot	Primality Proving with Elliptic Curves.	TPHOLs	2007	DBLP DOI BibTeX RDF
27	Steven Obua	Proving Bounds for Real Linear Programs in Isabelle/HOL.	TPHOLs	2005	DBLP DOI BibTeX RDF
27	César A. Muñoz, David R. Lester	Real Number Calculations and Theorem Proving.	TPHOLs	2005	DBLP DOI BibTeX RDF
27	Deepak Kapur, Nikita A. Sakhanenko	Automatic Generation of Generalization Lemmas for Proving Properties of Tail-Recursive Definitions.	TPHOLs	2003	DBLP DOI BibTeX RDF
27	Peter Dybjer, Qiao Haiyan, Makoto Takeyama	Combining Testing and Proving in Dependent Type Theory.	TPHOLs	2003	DBLP DOI BibTeX RDF
27	Konrad Slind, Joe Hurd	Applications of Polytypism in Theorem Proving.	TPHOLs	2003	DBLP DOI BibTeX RDF
27	Laurent Théry	Proving Pearl: Knuth's Algorithm for Prime Numbers.	TPHOLs	2003	DBLP DOI BibTeX RDF
27	Klaus Schneider 0001	Proving the Equivalence of Microstep and Macrostep Semantics.	TPHOLs	2002	DBLP DOI BibTeX RDF
27	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
27	Jason Hickey, Aleksey Nogin	Fast Tactic-Based Theorem Proving.	TPHOLs	2000	DBLP DOI BibTeX RDF
27	Roope Kaivola, Mark D. Aagaard	Divider Circuit Verification with Model Checking and Theorem Proving.	TPHOLs	2000	DBLP DOI BibTeX RDF
27	François Puitg, Jean-François Dufourd	Formal Specification and Theorem Proving Breakthroughs in Geometric Modeling.	TPHOLs	1998	DBLP DOI BibTeX RDF
27	Flemming Andersen, Kim Dam Petersen, Jimmi S. Pettersson	A Graphical Tool for Proving Unity Progress.	TPHOLs	1994	DBLP DOI BibTeX RDF
27	Holger Busch	First-Order Automation for Higher-Order-Logic Theorem Proving.	TPHOLs	1994	DBLP DOI BibTeX RDF
27	Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi	TPS: An Interactive and Automatic Tool for Proving Theorems of Type Theory.	HUG	1993	DBLP DOI BibTeX RDF
26	Jens Bendisposto, Michael Leuschel	Proof Assisted Model Checking for B.	ICFEM	2009	DBLP DOI BibTeX RDF	Model Checking, Experiment, Theorem Proving, B-Method, Tool Integration
26	Xia Wu, Jigui Sun, Shuai Lu 0001, Ying Li, Wei Meng, Minghao Yin	Improved Propositional Extension Rule.	RSKT	2006	DBLP DOI BibTeX RDF	Extension rule, reduced rule, theorem proving, propositional logic
26	Marcelo Glusman, Shmuel Katz	A Mechanized Proof Environment for the Convenient Computations Proof Method.	Formal Methods Syst. Des.	2003	DBLP DOI BibTeX RDF	convenient computations, proof environment, deductive theorem proving, formal verification, PVS
26	Herman Geuvers, Gueorgui I. Jojgov	Open Proofs and Open Terms: A Basis for Interactive Logic.	CSL	2002	DBLP DOI BibTeX RDF	open terms, meta-variables, formulas-as-types, type theory, interactive theorem proving
26	Sigrid Gürgens, Javier López 0001	Suitability of a Classical Analysis Method for E-commerce Protocols.	ISC	2001	DBLP DOI BibTeX RDF	electronic commerce, cryptographic protocol, Security analysis, automatic theorem proving, protocol validation
26	Myla Archer, Constance L. Heitmeyer, Elvinia Riccobene	Using TAME to prove invariants of automata models: Two case studies.	FMSP	2000	DBLP DOI BibTeX RDF	software requirements analysis, Software engineering, verification, formal methods, theorem proving
26	Mark D. Aagaard, Carl-Johan H. Seger	The formal verification of a pipelined double-precision IEEE floating-point multiplier.	ICCAD	1995	DBLP DOI BibTeX RDF	ANSI/IEEE Std 754-1985, model checking, theorem proving, floating-point arithmetic, Hardware verification
26	Li Dafa	An Application to Teaching in Logic Course of ATP Based Natural Deduction.	LPAR	1992	DBLP DOI BibTeX RDF	theorem proving, logic, natural deduction
26	Li Dafa	Intelligent CAI Course in the First-Order Logic.	ICCAL	1990	DBLP DOI BibTeX RDF	tautology, theorem proving, first-order logic, resolution, natural deduction
26	Myla Archer, Hongping Lim, Nancy A. Lynch, Sayan Mitra, Shinya Umeno	Specifying and proving properties of timed I/O automata in the TIOA toolkit.	MEMOCODE	2006	DBLP DOI BibTeX RDF
26	Devrim Unal, M. Ufuk Çaglayan	Theorem proving for modeling and conflict checking of authorization policies.	ISCN	2006	DBLP DOI BibTeX RDF