Search results for "proofs"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
19	Kamal Aboul-Hosn	A Proof-Theoretic Approach to Tactics.	MKM	2006	DBLP DOI BibTeX RDF
19	Pedro Quaresma, Predrag Janicic	Integrating Dynamic Geometry Software, Deduction Systems, and Theorem Repositories.	MKM	2006	DBLP DOI BibTeX RDF
19	Matthias Baaz, Stefan Hetzl, Alexander Leitsch, Clemens Richter, Hendrik Spohr	Proof Transformation by CERES.	MKM	2006	DBLP DOI BibTeX RDF
19	Tetsu Iwata, Kaoru Kurosawa	How to Enhance the Security of the 3GPP Confidentiality and Integrity Algorithms.	FSE	2005	DBLP DOI BibTeX RDF
19	Ulrich Kohlenbach	Proof Mining in Functional Analysis.	CiE	2005	DBLP DOI BibTeX RDF
19	Nik Swoboda, Gerard Allwein	Using DAG transformations to verify Euler/Venn homogeneous and Euler/Venn FOL heterogeneous rules of inference.	Softw. Syst. Model.	2004	DBLP DOI BibTeX RDF	Euler and Venn diagrams, Graph transformation, Diagrammatic reasoning, Proof verification
19	Michael Soltys, Alasdair Urquhart	Matrix identities and the pigeonhole principle.	Arch. Math. Log.	2004	DBLP DOI BibTeX RDF
19	Nadeem Abdul Hamid, Zhong Shao, Valery Trifonov, Stefan Monnier, Zhaozhong Ni	A Syntactic Approach to Foundational Proof-Carrying Code.	J. Autom. Reason.	2003	DBLP DOI BibTeX RDF	foundational proof-carrying code, syntactic soundness proof, typed assembly language
19	Hirotada Kobayashi, Keiji Matsumoto, Tomoyuki Yamakami	Quantum Merlin-Arthur Proof Systems: Are Multiple Merlins More Helpful to Arthur?	ISAAC	2003	DBLP DOI BibTeX RDF
19	Josh Buresh-Oppenheim, Nicola Galesi, Shlomo Hoory, Avner Magen, Toniann Pitassi	Rank Bounds and Integrality Gaps for Cutting Planes Procedures Joshua.	FOCS	2003	DBLP DOI BibTeX RDF
19	Axel Schairer, Dieter Hutter	Proof Transformations for Evolutionary Formal Software Development.	AMAST	2002	DBLP DOI BibTeX RDF
19	Ivan Damgård, Eiichiro Fujisaki	A Statistically-Hiding Integer Commitment Scheme Based on Groups with Hidden Order.	ASIACRYPT	2002	DBLP DOI BibTeX RDF
19	Boaz Barak, Yehuda Lindell	Strict polynomial-time in simulation and extraction.	STOC	2002	DBLP DOI BibTeX RDF
19	Uwe Egly, Hans Tompits	Proof-complexity results for nonmonotonic reasoning.	ACM Trans. Comput. Log.	2001	DBLP DOI BibTeX RDF	default logic, circumscription, sequent calculi
19	James L. Caldwell	Extracting General Recursive Program Schemes in Nuprl's Type Theory.	LOPSTR	2001	DBLP DOI BibTeX RDF
19	Johan Håstad	Which NP-Hard Optimization Problems Admit Non-trivial Efficient Approximation Algorithms?	ICALP	2000	DBLP DOI BibTeX RDF
19	José Espírito Santo	Revisiting the Correspondence between Cut Elimination and Normalisation.	ICALP	2000	DBLP DOI BibTeX RDF
19	Fairouz Kamareddine, François Monin	On Automating Inductive and Non-inductive Termination Methods.	ASIAN	1999	DBLP DOI BibTeX RDF
19	Alexander A. Razborov	Lower Bounds for the Polynomial Calculus.	Comput. Complex.	1998	DBLP DOI BibTeX RDF	polynomial calculus, Proof complexity, pigeonhole principle
19	Myla Archer, Constance L. Heitmeyer	Human-Style Theorem Proving Using PVS.	TPHOLs	1997	DBLP DOI BibTeX RDF
19	Deepak Kapur, Mahadevan Subramaniam	Mechanically Verifying a Family of Multiplier Circuits.	CAV	1996	DBLP DOI BibTeX RDF
19	Harry Buhrman, Thomas Thierauf	The Complexity of Generating and Checking Proffs of Membership.	STACS	1996	DBLP DOI BibTeX RDF
19	Alberto Coen-Porisini, Richard A. Kemmerer, Dino Mandrioli	A Formal Framework for ASTRAL Intralevel Proof Obligations.	IEEE Trans. Software Eng.	1994	DBLP DOI BibTeX RDF	intralevel proof obligations, formal software development, mathematical correctness, ASLAN, TRIO, real-time systems, real-time systems, verification, formal specification, formal specification, formal methods, finite state machines, program verification, specification languages, state machines, formal specification language, formal proof, timing requirements, ASTRAL
19	Martin Protzen	Lazy Generation of Induction Hypotheses.	CADE	1994	DBLP DOI BibTeX RDF
19	Toby Walsh, Alex Nunes, Alan Bundy	The Use of Proof Plans to Sum Series.	CADE	1992	DBLP DOI BibTeX RDF
19	Seppo Keronen	Natural Deduction Proof Theory for Logic Programming.	ELP	1992	DBLP DOI BibTeX RDF
19	Andrei Voronkov	On Completeness of Program Synthesis Systems.	CSL	1991	DBLP DOI BibTeX RDF
18	Holger Dell, Dieter van Melkebeek	Satisfiability allows no nontrivial sparsification unless the polynomial-time hierarchy collapses.	STOC	2010	DBLP DOI BibTeX RDF	arithmetic progression free sets, hereditary graph properties, vertex deletion problems, satisfiability, kernelization, vertex cover, parameterized complexity, probabilistically checkable proofs, feedback vertex set, sparsification
18	Jean-François Dufourd	An Intuitionistic Proof of a Discrete Form of the Jordan Curve Theorem Formalized in Coq with Combinatorial Hypermaps.	J. Autom. Reason.	2009	DBLP DOI BibTeX RDF	Computer-aided proofs, Coq system, Combinatorial hypermaps, Discrete Jordan Curve Theorem, Formal specifications, Computational topology, Planar subdivisions
18	Peter Verdée, Stephan van der Waart van Gulik	A Generic Framework for Adaptive Vague Logics.	Stud Logica	2008	DBLP DOI BibTeX RDF	supervaluationism, subvaluationism, clarity logic, dynamic proofs, fuzzy logic, vagueness, adaptive logic
18	Irene Polycarpou	Induction as a tool for conceptual coherence in computer science.	ACM Southeast Regional Conference	2008	DBLP DOI BibTeX RDF	undergraduate computer science curricula, computer science education, structural induction, proofs by induction
18	Scott Aaronson, Avi Wigderson	Algebrization: a new barrier in complexity theory.	STOC	2008	DBLP DOI BibTeX RDF	communication complexity, oracles, arithmetization, interactive proofs, query complexity, low-degree polynomials
18	Martin Nordio, Peter Müller 0001, Bertrand Meyer 0001	Proof-Transforming Compilation of Eiffel Programs.	TOOLS (46)	2008	DBLP DOI BibTeX RDF	proof-transforming compiler, CIL, Software verification, Proof-Carrying Code, Eiffel, program proofs
18	Dana Moshkovitz, Ran Raz	Sub-constant error low degree test of almost-linear size.	STOC	2006	DBLP DOI BibTeX RDF	plane vs. point test, probabilistically checkable proofs, locally testable codes, low degree testing
18	Alex Samorodnitsky, Luca Trevisan	Gowers uniformity, influence of variables, and PCPs.	STOC	2006	DBLP DOI BibTeX RDF	influence of variables, probabilistically checkable proofs, linearity test
18	Rafael Pass, Abhi Shelat, Vinod Vaikuntanathan	Construction of a Non-malleable Encryption Scheme from Any Semantically Secure One.	CRYPTO	2006	DBLP DOI BibTeX RDF	Non-interactive Zero-knowledge Proofs, Public-key Encryption, Semantic Security, Non-malleability
18	Eli Ben-Sasson, Madhu Sudan 0001	Simple PCPs with poly-log rate and query complexity.	STOC	2005	DBLP DOI BibTeX RDF	PCPP, probabilistically checkable proofs, PCP, locally testable codes
18	Eli Ben-Sasson, Oded Goldreich 0001, Prahladh Harsha, Madhu Sudan 0001, Salil P. Vadhan	Robust pcps of proximity, shorter pcps and applications to coding.	STOC	2004	DBLP DOI BibTeX RDF	property testing, probabilistically checkable proofs, PCP, locally decodable codes, locally testable codes
18	Aggelos Kiayias, Moti Yung	Non-interactive Zero-Sharing with Applications to Private Distributed Decision Making.	Financial Cryptography	2003	DBLP DOI BibTeX RDF	Veto, Simultaneous Disclosure, Privacy, Electronic Voting, Distributed Decision Making, Proofs of Knowledge
18	Bartosz Przydatek, Dawn Xiaodong Song, Adrian Perrig	SIA: secure information aggregation in sensor networks.	SenSys	2003	DBLP DOI BibTeX RDF	security, sensor networks, approximate, interactive proofs, information aggregation
18	Yasuhiko Minamide, Koji Okuma	Verifying CPS transformations in Isabelle/HOL.	MERLIN	2003	DBLP DOI BibTeX RDF	program transformation, theorem proving, correctness proofs
18	Mihir Bellare, Bennet S. Yee	Forward-Security in Private-Key Cryptography.	CT-RSA	2003	DBLP DOI BibTeX RDF	pseudorandom bit generators, message authentication, forward security, Symmetric cryptography, audit logs, proofs of security
18	Eli Ben-Sasson, Madhu Sudan 0001, Salil P. Vadhan, Avi Wigderson	Randomness-efficient low degree tests and short PCPs via epsilon-biased sets.	STOC	2003	DBLP DOI BibTeX RDF	property testing, probabilistically checkable proofs, locally testable codes, linearity testing, low degree testing
18	Matthias Baaz, Georg Moser	On Generalizations of Semi-terms of Particularly Simple Form.	CSL	2002	DBLP DOI BibTeX RDF	Structure of Proofs, Complexity of Programs, Proof Theory
18	Peter Dybjer, Anton Setzer	Indexed Induction-Recursion.	Proof Theory in Computer Science	2001	DBLP DOI BibTeX RDF	Dependent type theory, Martin-Löf Type Theory, inductive-recursive definitions, inductive families, normalization proofs, generic programming, inductive definitions, initial algebras
18	Dan Grossman, J. Gregory Morrisett, Steve Zdancewic	Syntactic type abstraction.	ACM Trans. Program. Lang. Syst.	2000	DBLP DOI BibTeX RDF	proof techniques, syntactic proofs, type abstraction, operational semantics, parametricity
18	Adam L. Young, Moti Yung	Towards Signature-Only Signature Schemes.	ASIACRYPT	2000	DBLP DOI BibTeX RDF	Public Key Cryptosystems (PKCS), nested trapdoor, abuse freeness, (subliminal) leakage, design validation proofs, FIPS, digital signature, decryption, Public Key Infrastructure (PKI), NIST
18	Anna Gál, Shai Halevi, Richard J. Lipton, Erez Petrank	Computing from Partial Solutions.	CCC	1999	DBLP DOI BibTeX RDF	Robust proofs, erasure correction, erasure-resilient reductions, fault tolerant computations, NP-Hardness
18	Gerrit Bleumer	Biometric yet Privacy Protecting Person Authentication.	Information Hiding	1998	DBLP DOI BibTeX RDF	Non-transferable certificates, Wallets-with-observer, Biometric person authentication, Blind Signatures, Interactive proofs
18	Farokh B. Bastani, Bojan Cukic	Impact of program transformation on software reliability assessment.	HASE	1996	DBLP DOI BibTeX RDF	statistical sampling method, complete program paths, partial proofs, reliability assessment procedure, formal methods, program transformation, program verification, correctness, software fault tolerance, safety critical software, test cases, operational profile, reliability estimate, software reliability assessment
18	Mats Per Erik Heimdahl, Barbara J. Czerny	Using PVS to analyze hierarchical state-based requirements for completeness and consistency.	HASE	1996	DBLP DOI BibTeX RDF	hierarchical state based requirements specifications, input sequence, analysis procedures, large real world requirements specification, hierarchical state based language, Requirements State Machine Language, Prototype Verification System, theorem proving component, spurious error reports, formal specifications, robustness, consistency, program verification, completeness, Binary Decision Diagrams, BDDs, PVS, interactive environment, formal proofs, RSML
18	Souâd Taouil-Traverson, Sylvie Vignes	Preliminary Analysis Cycle for B-Method Software Development.	EUROMICRO	1996	DBLP DOI BibTeX RDF	preliminary analysis cycle, B-method software development, a priori errors detection, inconsistency deficiencies, formal specification, formal specifications, formal methods, correctness proofs, incompleteness, testing process, software life-cycle
18	Uriel Feige, Joe Kilian	Zero Knowledge and the Chromatic Number.	CCC	1996	DBLP DOI BibTeX RDF	approximation algorithms, zero knowledge, chromatic number, probabilistically checkable proofs
18	Ramayya Kumar, Thomas Kropf, Klaus Schneider 0001	Formal synthesis of circuits with a simple handshake protocol.	VLSI Design	1995	DBLP DOI BibTeX RDF	formal circuit synthesis, preproven building blocks, higher-order temporal operators, parametrized data signals, sequentially composed modules, parallel module composition, protocols, high level synthesis, logic design, operator semantics, template, formal logic, correctness proofs, synchronous circuits, handshake protocol, HOL theorem prover
18	Bruce W. Weide, Stephen H. Edwards, Douglas E. Harms, David Alex Lamb	Design and Specification of Iterators Using the Swapping Paradigm.	IEEE Trans. Software Eng.	1994	DBLP DOI BibTeX RDF	swapping paradigm, common interface model, user defined iterator abstractions, modular correctness proofs, formal specification, formal specification, formal methods, program verification, program verification, iterators, iterator designs, swapping, proof of correctness, modular reasoning, data encapsulation, imperative languages
18	Josyula R. Rao	Reasoning about Probabilistic Parallel Programs.	ACM Trans. Program. Lang. Syst.	1994	DBLP DOI BibTeX RDF	verification, parallel programming, probabilistic algorithms, correctness proofs, programming methodology, specification techniques
18	Matthias Anlauff, Stefan Jähnichen, Martin Simons 0001	An experimental support system for formal mathematical reasoning.	FME	1994	DBLP DOI BibTeX RDF	tool support, proofs, logical frameworks, formal reasoning
18	Mark G. Staskauskas	Formal Derivation of Concurrent Programs: An Example from Industry.	IEEE Trans. Software Eng.	1993	DBLP DOI BibTeX RDF	tapes, I/O channels, UNITY methodology, resource allocation algorithm, formal specification, parallel programming, specifications, operating system, program verification, concurrent programs, proofs, disks, formal derivation, I/O subsystem
18	Flemming Nielson, Hanne Riis Nielson	Layered Predicates.	REX Workshop	1992	DBLP DOI BibTeX RDF	partial equivalence relations, Kripke-logical relations, layered predicates, Kripke-layered predicates, substitution properties, well-structured proofs, correctness of code generation, proof principles, denotational semantics, logical relations
18	Laura K. Dillon	Verifying General Safety Properties of Ada Tasking Programs.	IEEE Trans. Software Eng.	1990	DBLP DOI BibTeX RDF	safety properties verification, Ada tasking programs, isolation approach, automating partial correctness proofs, Ada, program verification, concurrent programs, deadlock, mutual exclusion, symbolic execution, multiprocessing programs
18	Dipankar Sarkar 0001, S. C. De Sarkar	A Theorem Prover for Verifying Iterative Programs Over Integers.	IEEE Trans. Software Eng.	1989	DBLP DOI BibTeX RDF	rule-based theorem prover, iterative programs, overall proof construction strategy, array-sorting program, expert systems, theorem proving, program verification, performance measures, iterative methods, correctness proofs
18	R. Geoff Dromey	Systematic Program Development.	IEEE Trans. Software Eng.	1988	DBLP DOI BibTeX RDF	goal-oriented programming, case analysis, constructive program proofs, software engineering, data structure, refinements, programming, program development, problem decomposition, program structure, postcondition
18	Louis C. Guillou, Jean-Jacques Quisquater	A "Paradoxical" Indentity-Based Signature Scheme Resulting from Zero-Knowledge.	CRYPTO	1988	DBLP DOI BibTeX RDF	zero-knowledge interactive proofs, identity-based system, public key system, complexity, authentication, integrity, digital signature, randomization, identification, factoring, cryptology
18	C. A. R. Hoare	An Axiomatic Basis for Computer Programming.	Commun. ACM	1969	DBLP DOI BibTeX RDF	axiomatic method, formal language definition, machine-independent programming, program documentation, theory of programming' proofs of programs, programming language design
15	Jakob Schulz, Emin Karayel	Karatsuba Multiplication on Integers.	Arch. Formal Proofs	2024	DBLP BibTeX RDF
15	Axel Bergström, Tjark Weber	Verified QBF Solving.	Arch. Formal Proofs	2024	DBLP BibTeX RDF
15	Palle Raabjerg, Johannes Åman Pohjola, Tjark Weber	Broadcast Psi-calculi.	Arch. Formal Proofs	2024	DBLP BibTeX RDF
15	Ata Keskin	Doob's Upcrossing Inequality and Martingale Convergence Theorem.	Arch. Formal Proofs	2024	DBLP BibTeX RDF
15	Terru Stübinger, Lars Hupel	Go Code Generation for Isabelle.	Arch. Formal Proofs	2024	DBLP BibTeX RDF
15	Azucena Garvía Bosshard, Christoph Sprenger 0001, Jonathan Bootle	The Sumcheck Protocol.	Arch. Formal Proofs	2024	DBLP BibTeX RDF
15	Tobias Nipkow	Region Quadtrees.	Arch. Formal Proofs	2024	DBLP BibTeX RDF
15	Manuel Eberl	Kummer's congruence.	Arch. Formal Proofs	2024	DBLP BibTeX RDF
15	Sebastián Buss	Decomposition of totally ordered hoops.	Arch. Formal Proofs	2024	DBLP BibTeX RDF
15	Manuel Eberl	Continued Fractions.	Arch. Formal Proofs	2024	DBLP BibTeX RDF
15	Georg Struth, Tanguy Massacrier	Cubical Categories.	Arch. Formal Proofs	2024	DBLP BibTeX RDF
15	Peter Gammie	ConcurrentHOL.	Arch. Formal Proofs	2024	DBLP BibTeX RDF
15	Xavier Parent, Christoph Benzmüller	Conditional normative reasoning as a fragment of HOL (Isabelle/HOL dataset).	Arch. Formal Proofs	2024	DBLP BibTeX RDF
15	Achim D. Brucker, Amy Stell	(Extended) Interval Analysis.	Arch. Formal Proofs	2024	DBLP BibTeX RDF
15	Pasquale Noce	Information Flow Control via Stateful Intransitive Noninterference in Language IMP.	Arch. Formal Proofs	2024	DBLP BibTeX RDF
15	Jamie Chen	Wieferich-Kempner Theorem.	Arch. Formal Proofs	2024	DBLP BibTeX RDF
15	Cameron Calk, Georg Struth	Higher Globular Catoids and Quantales.	Arch. Formal Proofs	2024	DBLP BibTeX RDF
15	Alexander Treml	Uncertainty Principle.	Arch. Formal Proofs	2024	DBLP BibTeX RDF
15	Yong Kiam Tan, Jiong Yang	Approximate Model Counting.	Arch. Formal Proofs	2024	DBLP BibTeX RDF
15	Anders Schlichtkrull	Soundness of the Q0 proof system for higher-order logic.	Arch. Formal Proofs	2023	DBLP BibTeX RDF
15	Chelsea Edmonds	General Probabilistic Techniques for Combinatorics and the Lovasz Local Lemma.	Arch. Formal Proofs	2023	DBLP BibTeX RDF
15	Katharina Kreuzer, Manuel Eberl	Elimination of Repeated Factors Algorithm.	Arch. Formal Proofs	2023	DBLP BibTeX RDF
15	Emin Karayel	Distributed Distinct Elements.	Arch. Formal Proofs	2023	DBLP BibTeX RDF
15	Emin Karayel	Expander Graphs.	Arch. Formal Proofs	2023	DBLP BibTeX RDF
15	Anton Danilkin, Loïc Chevalier	Three Squares Theorem.	Arch. Formal Proofs	2023	DBLP BibTeX RDF
15	Benjamin Bisping, Luisa Montanari	Coupled Similarity and Contrasimilarity, and How to Compute Them.	Arch. Formal Proofs	2023	DBLP BibTeX RDF
15	Cárolos Laméris	Myhill-Nerode Theorem for Nominal G-Automata.	Arch. Formal Proofs	2023	DBLP BibTeX RDF
15	Chelsea Edmonds, Lawrence C. Paulson	Hypergraph Colouring Bounds.	Arch. Formal Proofs	2023	DBLP BibTeX RDF
15	Manuel Eberl	Lambert Series.	Arch. Formal Proofs	2023	DBLP BibTeX RDF
15	Anthony Bordg, Adrián Doña Mateo	Strict Omega Categories.	Arch. Formal Proofs	2023	DBLP BibTeX RDF
15	Ata Keskin	Eudoxus Reals.	Arch. Formal Proofs	2023	DBLP BibTeX RDF
15	Frank J. Balbach	The Cook-Levin theorem.	Arch. Formal Proofs	2023	DBLP BibTeX RDF
15	Andrei Popescu 0001	Renaming-Enriched Sets (Rensets) and Renaming-Based Recursion.	Arch. Formal Proofs	2023	DBLP BibTeX RDF
15	Mathias Schack Rabing	Ceva's Theorem.	Arch. Formal Proofs	2023	DBLP BibTeX RDF
15	Maximilian Spitz	Gray Codes for Arbitrary Numeral Systems.	Arch. Formal Proofs	2023	DBLP BibTeX RDF
15	Rodrigo Raya	Group Law of Edwards Elliptic Curves.	Arch. Formal Proofs	2023	DBLP BibTeX RDF