Search results for "correctness proofs"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
2	Matthias F. Stallmann, Suzanne Balik, Robert D. Rodman, Sina Bahram, Michael C. Grace, Susan D. High	ProofChecker: an accessible environment for automata theory correctness proofs.	ITiCSE	2007	DBLP DOI BibTeX RDF	accessibility, finite automata, correctness proof
2	Kamel Barkaoui, Claude Kaiser, Jean-François Pradat-Peyre	Petri nets based proofs of Ada 95 solution for preference control.	APSEC	1997	DBLP DOI BibTeX RDF	Petri nets based proofs, preference control, dining philosophers paradigm, entry families, requeue statements, Petri nets, deadlock, colored Petri nets, Ada 95, correctness proofs, starvation, protected objects
2	Willem C. Mallon, Jan Tijmen Udding	Using Metrics for Proof Rules for Recursively Defined Delay-insensitive Specifications.	ASYNC	1997	DBLP DOI BibTeX RDF	delay-insensitive specifications, recursive definition, linear proofs, intuitive induction rule, algebraic specification, algebraic specifications, theorem provers, correctness proofs, proof rules, proof rule
2	Alessandro Armando, Alan Smaill, Ian Green	Automatic Synthesis of Recursive Programs: The Proof-Planning Paradigm. (PDF / PS)	ASE	1997	DBLP DOI BibTeX RDF	proof-planning paradigm, recursive functional programs, functional programming, correctness proofs, automatic synthesis, recursive programs, unification algorithm
2	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
2	Ramayya Kumar, Thomas Kropf, Klaus Schneider	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
2	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
2	Joseph Y. Halpern, Lenore D. Zuck	A Little Knowledge Goes a Long Way: Knowledge-Based Derivations and Correctness Proofs for a Family of Protocols.	J. ACM	1992	DBLP DOI BibTeX RDF	reasoning about knowledge
2	G. A. Venkatesh, Charles N. Fischer	SPARE: A Development Environment For Program Analysis Algorithms.	IEEE Trans. Software Eng.	1992	DBLP DOI BibTeX RDF	program analysis specifications, high-level specification language, SPARE, structured program analysis refinement environment, denotational specification, formal specification, testing, software tools, software tools, programming environments, specification languages, program testing, development environment, correctness proofs
2	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
2	D. Sarkar, 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
2	Laurian M. Chirica, David F. Martin	Toward Compiler Implementation Correctness Proofs.	ACM Trans. Program. Lang. Syst.	1986	DBLP DOI BibTeX RDF
2	Gilles Bernot, Michel Bidoit, Christine Choppy	Abstract Implementations and Correctness Proofs.	STACS	1986	DBLP DOI BibTeX RDF
1	Holger Gast	Developer-Oriented Correctness Proofs - A Case Study of Cheney's Algorithm.	ICFEM	2011	DBLP DOI BibTeX RDF
1	Tim A. C. Willemse	Consistent Correlations for Parameterised Boolean Equation Systems with Applications in Correctness Proofs for Manipulations.	CONCUR	2010	DBLP DOI BibTeX RDF
1	Matthias Heizmann, Jochen Hoenicke, Andreas Podelski	Nested interpolants.	POPL	2010	DBLP DOI BibTeX RDF	floyd-hoare logic, nested words, static analysis, interpolants, abstract interpretation, recursion, software model checking, abstraction refinement
1	Ji-Cherng Lin, Ming-Yi Chiu	Short correctness proofs for two self-stabilizing algorithms under the distributed daemon model.	Discrete Applied Mathematics	2009	DBLP DOI BibTeX RDF
1	Adam Chlipala, J. Gregory Malecha, Greg Morrisett, Avraham Shinnar, Ryan Wisnesky	Effective interactive proofs for higher-order imperative programs.	ICFP	2009	DBLP DOI BibTeX RDF	functional programming, dependent types, separation logic, interactive proof assistants
1	Saurabh Srivastava, Sumit Gulwani	Program verification using templates over predicate abstraction.	PLDI	2009	DBLP DOI BibTeX RDF	constraint-based fixed-point, iterative fixed-point, quantified invariants, template invariants, predicate abstraction, weakest preconditions, smt solvers
1	Daniel Wasserrab, Denis Lohner, Gregor Snelting	On PDG-based noninterference and its modular proof.	PLAS	2009	DBLP DOI BibTeX RDF	modularity, program slicing, noninterference, correctness proof, program dependence graph
1	Karen Zee, Viktor Kuncak, Martin C. Rinard	An integrated proof language for imperative programs.	PLDI	2009	DBLP DOI BibTeX RDF	verification, theorem prover, proof system
1	Raimundo José de Araújo Macêdo, Sérgio Gorender	Perfect Failure Detection in the Partitioned Synchronous Distributed System Model.	ARES	2009	DBLP DOI BibTeX RDF
1	Yuxin Deng, Jean-François Monin	Verifying Self-stabilizing Population Protocols with Coq.	TASE	2009	DBLP DOI BibTeX RDF
1	Bernd Fischer 0002, Ando Saabas, Tarmo Uustalu	Program Repair as Sound Optimization of Broken Programs.	TASE	2009	DBLP DOI BibTeX RDF
1	Marieke Huisman, Alejandro Tamalet	A Formal Connection between Security Automata and JML Annotations.	FASE	2009	DBLP DOI BibTeX RDF
1	Mingwen Chen, Songlin Hu, Zhiyong Liu	Covering-Based Routing Algorithms for Cyclic Content-Based P/S System.	FAW	2009	DBLP DOI BibTeX RDF	cyclic topology, covering-based routing, content-based routing, publish/subscribe system
1	Simon Doherty, Mark Moir	Nonblocking Algorithms and Backward Simulation.	DISC	2009	DBLP DOI BibTeX RDF
1	Josef Widder, Ulrich Schmid	The Theta-Model: achieving synchrony without clocks.	Distributed Computing	2009	DBLP DOI BibTeX RDF	Clocks and time, Computing models, Partially synchronous systems, Fault-tolerant distributed algorithms
1	Filip Maric	Formalization and Implementation of Modern SAT Solvers.	J. Autom. Reasoning	2009	DBLP DOI BibTeX RDF	Algorithms, Data structures, Software verification, DPLL, SAT solving
1	Gergely Dévai	Programming Language Elements for Correctness Proofs.	Acta Cybern.	2008	DBLP BibTeX RDF
1	Jerry den Hartog	Towards mechanized correctness proofs for cryptographic algorithms: Axiomatization of a probabilistic Hoare style logic.	Sci. Comput. Program.	2008	DBLP DOI BibTeX RDF
1	Heidar Pirzadeh, Danny Dubé	Encoding the Program Correctness Proofs as Programs in PCC Technology.	PST	2008	DBLP DOI BibTeX RDF
1	Janis Voigtländer	Proving correctness via free theorems: the case of the destroy/build-rule.	PEPM	2008	DBLP DOI BibTeX RDF	intermediate data structures, rank-2 types, shortcut deforestation, theorems for free, program transformations, correctness proofs, relational parametricity
1	Tolga Ayav, Pascal Fradet, Alain Girault	Implementing fault-tolerance in real-time programs by automatic program transformations.	ACM Trans. Embedded Comput. Syst.	2008	DBLP DOI BibTeX RDF	Fault-tolerance, program transformations, checkpointing, correctness proofs, heartbeating
1	Thao Dang, Alexandre Donzé, Oded Maler, Noa Shalev	Sensitive state-space exploration.	CDC	2008	DBLP DOI BibTeX RDF
1	Yinian Qi, Mikhail J. Atallah	Efficient Privacy-Preserving k-Nearest Neighbor Search.	ICDCS	2008	DBLP DOI BibTeX RDF
1	Joe Kutner, Louise A. Perkins, Sumanth Yenduri, Farnaz Zand, Joe Zhang	AOP Maintains an Independent Coordinate System.	ITNG	2008	DBLP DOI BibTeX RDF
1	Aquinas Hobor, Andrew W. Appel, Francesco Zappa Nardelli	Oracle Semantics for Concurrent Separation Logic.	ESOP	2008	DBLP DOI BibTeX RDF
1	Heinrich Moser, Ulrich Schmid	Optimal Deterministic Remote Clock Estimation in Real-Time Systems.	OPODIS	2008	DBLP DOI BibTeX RDF	optimal clock synchronization, remote clock estimation, real-time systems, Distributed algorithms, computing models
1	Peeter Laud, Long Ngo	Threshold Homomorphic Encryption in the Universally Composable Cryptographic Library.	ProvSec	2008	DBLP DOI BibTeX RDF
1	Laurence Rideau, Bernard P. Serpette, Xavier Leroy	Tilting at Windmills with Coq: Formal Verification of a Compilation Algorithm for Parallel Moves.	J. Autom. Reasoning	2008	DBLP DOI BibTeX RDF	Parallel move, Parallel assignment, The Coq proof assistant, Compilation, Compiler correctness
1	Alberto Pettorossi, Maurizio Proietti, Valerio Senni	Automatic Correctness Proofs for Logic Program Transformations.	ICLP	2007	DBLP DOI BibTeX RDF
1	Roberto Segala, Andrea Turrini	Approximated Computationally Bounded Simulation Relations for Probabilistic Automata.	CSF	2007	DBLP DOI BibTeX RDF
1	Dong-Young Lee, Simon S. Lam	Protocol Design for Dynamic Delaunay Triangulation.	ICDCS	2007	DBLP DOI BibTeX RDF
1	Gary T. Leavens, Peter Müller	Information Hiding and Visibility in Interface Specifications.	ICSE	2007	DBLP DOI BibTeX RDF
1	Peter H. Schmitt, Isabel Tonin	Verifying the Mondex Case Study.	SEFM	2007	DBLP DOI BibTeX RDF
1	Maria João Frade, Ando Saabas, Tarmo Uustalu	Foundational certification of data-flow analyses.	TASE	2007	DBLP DOI BibTeX RDF	data-flow analyses, certification of analyses and optimizations, applied vs. foundational, type systems, program optimizations, Hoare logics, natural semantics
1	T. S. E. Maibaum	Challenges in Software Certification.	ICFEM	2007	DBLP DOI BibTeX RDF
1	Klaus Indermark, Thomas Noll	Algebraic Correctness Proofs for Compiling Recursive Function Definitions with Strictness Information.	Acta Inf.	2006	DBLP DOI BibTeX RDF	Stack implementation, Formal semantics, Functional languages, Evaluation strategies, Compiler correctness
1	Nicolas Guelfi, Amel Mammar	A formal framework to generate XPDL specifications from UML activity diagrams.	SAC	2006	DBLP DOI BibTeX RDF	XPDL language, transformations, correctness proofs, UML activity diagrams
1	Daniel Große, Ulrich Kühne, Rolf Drechsler	HW/SW co-verification of embedded systems using bounded model checking.	ACM Great Lakes Symposium on VLSI	2006	DBLP DOI BibTeX RDF	hardware/software co-verification, embedded systems, formal verification, SystemC, bounded model checking, PSL
1	Daniel Wasserrab, Tobias Nipkow, Gregor Snelting, Frank Tip	An operational semantics and type safety prooffor multiple inheritance in C++.	OOPSLA	2006	DBLP DOI BibTeX RDF	semantics, C++, type safety, multiple inheritance
1	Michal Armoni	On the role of proofs in a course on design and analysis of algorithms.	SIGCSE Bulletin	2006	DBLP DOI BibTeX RDF	algorithms, correctness, proof
1	Emerson Ribeiro de Mello, Savas Parastatidis, Philipp Reinecke, Chris Smith, Aad P. A. van Moorsel, Jim Webber	Secure and Provable Service Support for Human-Intensive Real-Estate Processes.	IEEE SCC	2006	DBLP DOI BibTeX RDF
1	Salahuddin Mohammad Masum, Amin Ahsan Ali	Maintaining a Binary Tree Structure For Mobile Ad Hoc Computing.	ISCC	2006	DBLP DOI BibTeX RDF
1	Andrew Ireland	Towards Automatic Assertion Refinement for Separation Logic.	ASE	2006	DBLP DOI BibTeX RDF
1	Tobias Gedell, Reiner Hähnle	Verification by Parallelization of Parametric Code.	Algebraic and Proof-theoretic Aspects of Non-classical Logics	2006	DBLP DOI BibTeX RDF
1	Amine Chaieb	Proof-Producing Program Analysis.	ICTAC	2006	DBLP DOI BibTeX RDF
1	Vadim Drabkin, Roy Friedman, Maria Gradinariu	Self-stabilizing Wireless Connected Overlays.	OPODIS	2006	DBLP DOI BibTeX RDF
1	Alexandru Salcianu, Konstantine Arkoudas	Machine-Checkable Correctness Proofs for Intra-procedural Dataflow Analyses.	Electr. Notes Theor. Comput. Sci.	2005	DBLP DOI BibTeX RDF
1	Jan Olaf Blech, Sabine Glesner, Johannes Leitner, Steffen Mülling	Optimizing Code Generation from SSA Form: A Comparison Between Two Formal Correctness Proofs in Isabelle/HOL.	Electr. Notes Theor. Comput. Sci.	2005	DBLP DOI BibTeX RDF
1	Jianjun Duan, Joe Hurd, Guodong Li, Scott Owens, Konrad Slind, Junxing Zhang	Functional Correctness Proofs of Encryption Algorithms.	LPAR	2005	DBLP DOI BibTeX RDF
1	Emmanuil I. Marakakis	Guided Correctness Proofs of Logic Programs.	Artificial Intelligence and Applications	2005	DBLP BibTeX RDF
1	Sorin Lerner, Todd D. Millstein, Erika Rice, Craig Chambers	Automated soundness proofs for dataflow analyses and transformations via local rules.	POPL	2005	DBLP DOI BibTeX RDF	automated correctness proofs, compiler optimization
1	Haruo Hosoya, Jerome Vouillon, Benjamin C. Pierce	Regular expression types for XML.	ACM Trans. Program. Lang. Syst.	2005	DBLP DOI BibTeX RDF	XML, Type systems, subtyping
1	Malay K. Ganai, Aarti Gupta, Pranav Ashar	Verification of Embedded Memory Systems using Efficient Memory Modeling.	DATE	2005	DBLP DOI BibTeX RDF
1	Kamel Adi, Liviu Pene	Secrecy Correctness for Security Protocols.	DFMA	2005	DBLP DOI BibTeX RDF	Protocol Correctness, Security Protocols, Formal Analysis, Secrecy
1	Sven Beyer, Peter Böhm, Michael Gerke 0002, Mark A. Hillebrand, Thomas In der Rieden, Steffen Knapp, Dirk Leinenbach, Wolfgang J. Paul	Towards the Formal Verification of Lower System Layers in Automotive Systems.	ICCD	2005	DBLP DOI BibTeX RDF
1	Taolue Chen, Tingting Han, Jian Lu	Analysis of A Leader Election Algorithm in uCRL.	CIT	2005	DBLP DOI BibTeX RDF
1	Rong Peng, Jingsong Cui, Yue Pan	Efficient Deadlock-Freeness Detection in Real-time Systems.	CIT	2005	DBLP DOI BibTeX RDF
1	Daniel Große, Ulrich Kühne, Rolf Drechsler	HW/SW Co-Verification of a RISC CPU using Bounded Model Checking.	MTV	2005	DBLP DOI BibTeX RDF
1	David Pichardie	Modular Proof Principles for Parameterised Concretizations.	CASSIS	2005	DBLP DOI BibTeX RDF
1	Thomas In der Rieden, Dirk Leinenbach, Wolfgang J. Paul	Towards the Pervasive Verification of Automotive Systems.	CHARME	2005	DBLP DOI BibTeX RDF
1	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
1	Pawel T. Wojciechowski, Olivier Rütti	On Correctness of Dynamic Protocol Update.	FMOODS	2005	DBLP DOI BibTeX RDF
1	Lars Grunske, Peter A. Lindsay, Nisansala Yatapanage, Kirsten Winter	An Automated Failure Mode and Effect Analysis Based on High-Level Design Specification with Behavior Trees.	IFM	2005	DBLP DOI BibTeX RDF	Automated Hazard Analysis, High-Level Design Specification, Model Checking, FMEA, SAL, Behavior Trees
1	Benjamin Grégoire, Assia Mahboubi	Proving Equalities in a Commutative Ring Done Right in Coq.	TPHOLs	2005	DBLP DOI BibTeX RDF
1	Jan Friso Groote, François Monin, Jan Springintveld	A computer checked algebraic verification of a distributed summation algorithm.	Formal Asp. Comput.	2005	DBLP DOI BibTeX RDF	Distributed summation algorithm, Formal proof checking, Verification, Process algebra, PVS, CRL
1	Douglas Gregor, Jaakko Järvi, Mayuresh Kulkarni, Andrew Lumsdaine, David R. Musser, Sibylle Schupp	Generic Programming and High-Performance Libraries.	International Journal of Parallel Programming	2005	DBLP DOI BibTeX RDF	high-level optimization, formal verification, static analysis, Generic programming, software libraries
1	Nick Benton	Simple relational correctness proofs for static analyses and program transformations.	POPL	2004	DBLP DOI BibTeX RDF	partial equivalence relations, security, dependency, program analysis, information flow, types, optimizing compilation, denotational semantics, Hoare logic
1	Patricia Johann, Janis Voigtländer	Free theorems in the presence of seq.	POPL	2004	DBLP DOI BibTeX RDF	controlling strict evaluation, short cut fusion, theorems for free, program transformations, Haskell, denotational semantics, parametricity, correctness proofs, logical relations
1	Fubo Zhang, Erik H. D'Hollander	Using Hammock Graphs to Structure Programs.	IEEE Trans. Software Eng.	2004	DBLP DOI BibTeX RDF	optimization, parallel processing, compilers, Program transformation, structured programming, correctness proofs, software/program verification
1	Carmen-Veronica Bobeanu, Eugene J. H. Kerckhoffs, Hendrik Van Landeghem	Modeling of discrete event systems: A holistic and incremental approach using Petri nets.	ACM Trans. Model. Comput. Simul.	2004	DBLP DOI BibTeX RDF	experimental frame, Petri nets, DEVS, structural modeling, Algebraic structures
1	Bernhard Beckert, Vladimir Klebanov	Proof Reuse for Deductive Program Verification.	SEFM	2004	DBLP DOI BibTeX RDF
1	Bertrand Jeannet, Wendelin Serwe	Abstracting Call-Stacks for Interprocedural Verification of Imperative Programs.	AMAST	2004	DBLP DOI BibTeX RDF
1	Marc Aiguier, Stefan Béroff, Pierre-Yves Schobbens	An Algebraic Approach for Codesign.	ICTAC	2004	DBLP DOI BibTeX RDF
1	Alan Stewart, Maurice Clint, Joaquim Gabarró	Barrier synchronisation: Axiomatisation and relaxation.	Formal Asp. Comput.	2004	DBLP DOI BibTeX RDF	Global synchronisation, Operation relaxation, High performance computing, Hoare logic, BSP
1	Béatrice Bérard, Laurent Fribourg, Francis Klay, Jean-François Monin	Compared Study of Two Correctness Proofs for the Standardized.	Formal Methods in System Design	2003	DBLP DOI BibTeX RDF
1	Yasuhiko Minamide, Koji Okuma	Verifying CPS transformations in Isabelle/HOL.	MERLIN	2003	DBLP DOI BibTeX RDF	program transformation, theorem proving, correctness proofs
1	Rex L. Page	Software is discrete mathematics.	ICFP	2003	DBLP DOI BibTeX RDF	software engineering, formal methods, functional programming, correctness proofs, discrete mathematics, predicate logic
1	Sorin Lerner, Todd D. Millstein, Craig Chambers	Automatically proving the correctness of compiler optimizations.	PLDI	2003	DBLP DOI BibTeX RDF	automated correctness proofs, compiler optimization
1	Anupam Datta, Ante Derek, John C. Mitchell, Dusko Pavlovic	A Derivation System for Security Protocols and its Logical Formalization.	CSFW	2003	DBLP DOI BibTeX RDF
1	Bernhard Beckert, Peter H. Schmitt	Program Verification Using Change Information.	SEFM	2003	DBLP DOI BibTeX RDF
1	Maria-Cristina V. Marinescu, Martin C. Rinard	A Formal Framework for Modular Synchronous System Design.	FME	2003	DBLP DOI BibTeX RDF	modular, system design, asynchronous, formal
1	Heike Wehrheim	Inheritance of Temporal Logic Properties.	FMOODS	2003	DBLP DOI BibTeX RDF
1	Patrice Godefroid, Radha Jagadeesan	On the Expressiveness of 3-Valued Models.	VMCAI	2003	DBLP DOI BibTeX RDF
1	Paul C. Attie	On the Implementation Complexity of Specifications of Concurrent Programs.	DISC	2003	DBLP DOI BibTeX RDF
1	Bertrand Meyer	Towards Practical Proofs of Class Correctness.	ZB	2003	DBLP DOI BibTeX RDF
1	Galina Jalal, Jakob Krarup	Geometrical Solution to the Fermat Problem with Arbitrary Weights.	Annals OR	2003	DBLP DOI BibTeX RDF	locational decisions, Fermat, positive and negative weights, plane geometry
1	Janis Voigtländer	Concatenate, reverse and map vanish for free.	ICFP	2002	DBLP DOI BibTeX RDF	list abstraction, rank-2 types, shortcut deforestation, the concatenate vanishes, theorems for free, program transformation, denotational semantics, combinators, parametricity, correctness proofs