Search results for "program verification"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
3	Naoki Kobayashi, Naoshi Tabuchi, Hiroshi Unno	Higher-order multi-parameter tree transducers and recursion schemes for program verification.	POPL	2010	DBLP DOI BibTeX RDF	higher-order tree transducers, tree-processing programs, program verification, higher-order recursion scheme
3	Huu Hai Nguyen, Wei-Ngan Chin	Enhancing Program Verification with Lemmas.	CAV	2008	DBLP DOI BibTeX RDF	Lemma Proving, Lemma Application, Program Verification, Separation Logic, Entailment
3	Bican Xia, Lu Yang, Naijun Zhan	Program Verification by Reduction to Semi-algebraic Systems Solving.	ISoLA	2008	DBLP DOI BibTeX RDF	Semi-Algebraic Systems, Program Verification, Invariants, Quantifier Elimination, Ranking Functions, Polynomial Programs
3	Michael Jackson	What Can We Expect from Program Verification?	IEEE Computer	2006	DBLP DOI BibTeX RDF	software engineering, program verification, system reliability, software-intensive systems
3	Lu Yang, Naijun Zhan, Bican Xia, Chaochen Zhou	Program Verification by Using DISCOVERER.	VSTTE	2005	DBLP DOI BibTeX RDF	semi-algebraic systems, DISCOVERER, reachability computation, program verification, termination, invariant generation
3	Tjark Weber	Towards Mechanized Program Verification with Separation Logic.	CSL	2004	DBLP DOI BibTeX RDF	Separation Logic, Interactive Theorem Proving, Formal Program Verification
3	Nicolas Halbwachs, Fabienne Lagnier, Christophe Ratel	Programming and Verifying Real-Time Systems by Means of the Synchronous Data-Flow Language LUSTRE.	IEEE Trans. Software Eng.	1992	DBLP DOI BibTeX RDF	data-flow language LUSTRE, synchronous data-flow language, critical real-time systems, ergonomy, dataflow approach, traditional description tools, verification tool LESAR, critical properties, real-time systems, parallel programming, program verification, program verification, parallel languages, verification methods, formal design
3	Sergio Cárdenas-García, Marvin V. Zelkowitz	A Management Tool For Evaluation of Software Designs.	IEEE Trans. Software Eng.	1991	DBLP DOI BibTeX RDF	economic decision theory, prototyping investigative system, equilibrium probabilities, software tools, decision support system, decision support systems, program verification, program verification, software designs, software prototyping, risk analysis, functional model, evaluation strategy, Selector, management tool
3	D. Sarkar, S. C. De Sarkar	A Set of Inference Rules for Quantified Formula Handling and Array Handling in Verification of Programs Over Integers.	IEEE Trans. Software Eng.	1989	DBLP DOI BibTeX RDF	quantified formula handling, array handling, undecidability problem, automated verifier, quantified formulas, bound-extension rule, bound-modification, theorem proving, program verification, program verification, first-order logic, inference mechanisms, decidability, inference rules, integer arithmetic
2	Saurabh Srivastava, Sumit Gulwani, Jeffrey S. Foster	From program verification to program synthesis.	POPL	2010	DBLP DOI BibTeX RDF	proof-theoretic program synthesis, verification
2	Tomas Kalibera, Pavel Parizek, Ghaith Haddad, Gary T. Leavens, Jan Vitek	Challenge benchmarks for verification of real-time programs.	PLPV	2010	DBLP DOI BibTeX RDF	java, verification, real-time
2	Wolfgang Schreiner	The RISC ProofNavigator: a proving assistant for program verification in the classroom.	Formal Asp. Comput.	2009	DBLP DOI BibTeX RDF	Interactive proving assistants, Teaching formal methods, Computer-aided verification
2	Levent Erkök, John Matthews	Pragmatic equivalence and safety checking in Cryptol.	PLPV	2009	DBLP DOI BibTeX RDF	sat/smt solving, size polymorphism, formal methods, cryptography, theorem proving, equivalence checking
2	Nurlida Basir, Ewen Denney, Bernd Fischer 0002	Constructing a Safety Case for Automatically Generated Code from Formal Program Verification Information.	SAFECOMP	2008	DBLP DOI BibTeX RDF	Goal Structuring Notation, Hoare logic, fault tree analysis, Automated code generation, safety case, formal program verification
2	Sebastian Burckhardt, Madanlal Musuvathi	Effective Program Verification for Relaxed Memory Models.	CAV	2008	DBLP DOI BibTeX RDF
2	Li Li, Ming Gu, Xiaoyu Song, Jianmin Wang 0001	Effective Predicate Abstraction for Program Verification.	TASE	2008	DBLP DOI BibTeX RDF	program verification, predicate abstraction
2	Hélène Collavizza, Michel Rueher, Pascal Van Hentenryck	CPBPV: A Constraint-Programming Framework for Bounded Program Verification.	CP	2008	DBLP DOI BibTeX RDF
2	Ewen Denney, Bernd Fischer 0002	Generating customized verifiers for automatically generated code.	GPCE	2008	DBLP DOI BibTeX RDF	logical annotations, program verification, automated theorem proving, hoare logic, software certification, automated code generation
2	Sumit Gulwani, Saurabh Srivastava, Ramarathnam Venkatesan	Program analysis as constraint solving.	PLDI	2008	DBLP DOI BibTeX RDF	most-general counterexamples, non-termination analysis, strongest postcondition, program verification, constraint solving, weakest precondition, bounds analysis
2	Ana Cristina Vieira de Melo, Paulo R. F. Nunes, Kleber S. Xavier	Towards verification and testing of Java programs.	SAC	2008	DBLP DOI BibTeX RDF	program verification, java programs, object-oriented testing
2	Li Li, Xiaoyu Song, Ming Gu, Jianmin Wang 0001	A Maximum Weight Heuristic Method for Abstract State Computation.	COMPSAC	2008	DBLP DOI BibTeX RDF	model checking, program verification, weight, predicate abstraction
2	Elvira Albert, Germán Puebla, Manuel V. Hermenegildo	Abstraction-Carrying Code: a Model for Mobile Code Safety.	New Generation Comput.	2008	DBLP DOI BibTeX RDF	Mobile Code Safety, Logic Programming, Static Analysis, Abstract Interpretation, Program Verification
2	Karen Zee, Viktor Kuncak, Michael Taylor, Martin C. Rinard	Runtime Checking for Program Verification.	RV	2007	DBLP DOI BibTeX RDF
2	Sumit Gulwani, Nebojsa Jojic	Program verification as probabilistic inference.	POPL	2007	DBLP DOI BibTeX RDF	automated recovery machine, forward and backward analysis, over and under approximation, learning, program verification, Markov chain Monte Carlo, Gibbs sampling, belief networks, probabilistic inference, factor graphs
2	Paritosh Shroff, Christian Skalka, Scott F. Smith	The Nuggetizer: Abstracting Away Higher-Orderness for Program Verification.	APLAS	2007	DBLP DOI BibTeX RDF	0CFA, program analysis, program verification, higher-order
2	Nicolas Oury	Pattern matching coverage checking with dependent types using set approximations.	PLPV	2007	DBLP DOI BibTeX RDF	coverage checking, set approximation, pattern matching
2	Alexei Lisitsa, Andrei P. Nemytykh	A Note on Specialization of Interpreters.	CSR	2007	DBLP DOI BibTeX RDF	program verification, cache coherence protocols, Program specialization, supercompilation
2	Philipp Rümmer, Muhammad Ali Shah	Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic.	TAP	2007	DBLP DOI BibTeX RDF	Disproving, Testing, Program verification, Program logics
2	Patrice Chalin	Are the Logical Foundations of Verifying Compiler Prototypes Matching user Expectations?	Formal Asp. Comput.	2007	DBLP DOI BibTeX RDF	Logical foundations, Static program verification, Survey, Assertions, Design by contract, Industrial practice, Extended static checking, Runtime assertion checking
2	Zhou Chaochen	Program Verification Through Computer Algebra.	ICFEM	2006	DBLP DOI BibTeX RDF
2	Cong-Cong Xing	Enhancing program verifications by restricting object types.	SAC	2006	DBLP DOI BibTeX RDF	object types, OOP, program verification
2	Bernhard Beckert, Steffen Schlager, Peter H. Schmitt	An Improved Rule for While Loops in Deductive Program Verification.	ICFEM	2005	DBLP DOI BibTeX RDF
2	Willem-Paul de Roever	A Perspective on Program Verification.	VSTTE	2005	DBLP DOI BibTeX RDF
2	Bernhard Beckert, Vladimir Klebanov	Proof Reuse for Deductive Program Verification.	SEFM	2004	DBLP DOI BibTeX RDF
2	Isabelle Dony, Baudouin Le Charlier	A Program Verification System Based on Oz.	MOZ	2004	DBLP DOI BibTeX RDF
2	Byron Cook, Daniel Kroening, Natasha Sharygina	Accurate Theorem Proving for Program Verification.	ISoLA	2004	DBLP DOI BibTeX RDF
2	Nils Anders Danielsson, Patrik Jansson	Chasing Bottoms: A Case Study in Program Verification in the Presence of Partial and Infinite Values.	MPC	2004	DBLP DOI BibTeX RDF
2	Grace Tsai, Shuhua Wang	Using Program Transformations to Provide Safety Properties for Real-Time Systems.	Real-Time Systems	2004	DBLP DOI BibTeX RDF	fault tolerance, real time systems, formal methods, temporal logic, program verification, executable assertions
2	Hongwei Xi	Facilitating Program Verification with Dependent Types.	SEFM	2003	DBLP DOI BibTeX RDF
2	Bart Jacobs, Erik Poll	Java Program Verification at Nijmegen: Developments and Perspective.	ISSS	2003	DBLP DOI BibTeX RDF
2	Viktor Kuncak, Martin C. Rinard	Existential Heap Abstraction Entailment Is Undecidable.	SAS	2003	DBLP DOI BibTeX RDF	Program Verification, Shape Analysis, Type Checking, Monadic Second-Order Logic, Typestate, Graph Homomorphism, Post Correspondence Problem
2	Manuvir Das, Sorin Lerner, Mark Seigle	ESP: Path-Sensitive Program Verification in Polynomial Time.	PLDI	2002	DBLP DOI BibTeX RDF	error detection, dataflow analysis, path-sensitive analysis
2	Abhik Roychoudhury, Tulika Mitra	Specifying multithreaded Java semantics for program verification.	ICSE	2002	DBLP DOI BibTeX RDF	Java, JavaScript
2	Michael W. Whalen, Johann Schumann, Bernd Fischer 0002	Synthesizing Certified Code.	FME	2002	DBLP DOI BibTeX RDF	automatic program synthesis, code certification, program verification, automated theorem proving, proof-carrying code
2	Alvaro E. Arenas	An Abstract Model for Scheduling Real-Time Programs.	ICFEM	2002	DBLP DOI BibTeX RDF	Scheduling, Program Verification, Real-time Programming
2	Nevin Heintze, Joxan Jaffar, Razvan Voicu	A Framework for Combining Analysis and Verification.	POPL	2000	DBLP DOI BibTeX RDF	program analysis, abstract interpretation, program verification
2	Axel Dold, Vincent Vialard	Formal Verification of a Compiler Back-End Generic Checker Program.	Ershov Memorial Conference	1999	DBLP DOI BibTeX RDF	checker-based program verification, generic specification, formal verification
2	Annalisa Bossi, Nicoletta Cocco	Programs Without Failures.	LOPSTR	1997	DBLP DOI BibTeX RDF	finitely failing derivations, program transformation, program verification
2	Moshe Y. Vardi	Alternating Automata and Program Verification.	Computer Science Today	1995	DBLP DOI BibTeX RDF
2	Martina Schollmeyer, Bruce M. McMillin	Checking Program Proofs Made Eas. (PDF / PS)	COMPSAC	1995	DBLP DOI BibTeX RDF	temporal subsumption, proof checking, assertion-based reasoning, formal methods, program verification
2	William E. Howden, Bruce Wieand	QDA-A Method for Systematic Informal Program Analysis.	IEEE Trans. Software Eng.	1994	DBLP DOI BibTeX RDF	QDA, systematic informal program analysis, program properties, Quick Defect Analysis, comments analysis, abstract program model, hypothesis-driven method, operational flight program, formal specification, formal verification, specification, program verification, program verification, programming theory, program debugging, program diagnostics, program validity, code reading
2	David Lorge Parnas, Jan Madey, Michal Iglewski	Precise Documentation of Well-Structured Programs.	IEEE Trans. Software Eng.	1994	DBLP DOI BibTeX RDF	precise documentation, well-structured programs, program fragments, reference document, functional approach, program documentation, tabular form, software engineering, formal specification, specification, software maintenance, software maintenance, program verification, program verification, displays, software inspection, index, structured programming, lexicon, system documentation, program correctness
2	Scott D. Stoller	Addendum to ``Proof Rules for Flush Channels''.	IEEE Trans. Software Eng.	1994	DBLP DOI BibTeX RDF	flush channels, multiple identical messages, logic system, distributed systems, distributed processing, message passing, program verification, program verification, asynchronous communication, formal logic, channel, proof system, communicating processes, proof rules
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	Robert E. Strom, Daniel M. Yellin	Extending Typestate Checking Using Conditional Liveness Analysis.	IEEE Trans. Software Eng.	1993	DBLP DOI BibTeX RDF	typestate checking, conditional liveness analysis, uninitialized variable errors, dataflow analysis algorithm, statically tracked information, program verification, program verification, programming errors
2	Hanan Lutfiyya, Bruce M. McMillin, Alan Su 0002	Formal Derivation of an Error-Detecting Distributed Data Scheduler Using Changeling.	Formal Methods in Programming and Their Applications	1993	DBLP DOI BibTeX RDF	Concurrent Program Verification, Changeling, Fault Tolerance, Formal Methods, Distributed Databases, Transformation, Executable Assertions
2	Paresh B. Shah, James C. Pleasant	Formal program verification and computability theory.	ACM Southeast Regional Conference	1992	DBLP DOI BibTeX RDF	Hoare proof rules, loop programs, primitive recursive functions, computability theory, formal program verification
2	Maritta Heisel, Wolfgang Reif, Werner Stephan	Tactical Theorem Proving in Program Verification.	CADE	1990	DBLP DOI BibTeX RDF
2	James M. Morris, Mark Howard	Program Verification by Symbolic Execution of Hyperfinite Ideal Machines.	CAV	1990	DBLP DOI BibTeX RDF
2	Maritta Heisel, Wolfgang Reif, Werner Stephan	A Dynamic Logic for Program Verification.	Logic at Botik	1989	DBLP DOI BibTeX RDF
2	Raymond D. Gumb	A first course in program verification and the semantics of programming languages.	SIGCSE	1989	DBLP DOI BibTeX RDF
2	Abha Moitra, S. Sitharama Iyengar, Farokh B. Bastani, I-Ling Yen	Multilevel Data Structures: Models and Performance.	IEEE Trans. Software Eng.	1988	DBLP DOI BibTeX RDF	multilevel data structure, data structures, concurrency, software reliability, program verification, program verification, programming theory, correctness proof, data organization, maintenance processes
2	Leon Sterling, Alan Bundy	Meta-Level Inference and Program Verification.	CADE	1982	DBLP DOI BibTeX RDF	meta-level inference, logic programming, program verification
2	George W. Ernst, Raymond J. Hookway	The Use of Higher Order Logic in Program Verification.	IEEE Trans. Computers	1976	DBLP DOI BibTeX RDF	inductive assertions, program verification, Heuristic search, higher order logic, mechanical theorem proving
1	Stefan Hallerstede, Michael Leuschel	Experiments in program verification using Event-B.	Formal Asp. Comput.	2012	DBLP DOI BibTeX RDF
1	Zhiqiang Ren, Hongwei Xi	A Programmer-Centric Approach to Program Verification in ATS	CoRR	2012	DBLP BibTeX RDF
1	Koen Claessen, Nikhil Swamy (eds.)	Proceedings of the sixth workshop on Programming Languages meets Program Verification, PLPV 2012, Philadelphia, PA, USA, January 24, 2012	PLPV	2012	DBLP BibTeX RDF
1	Martin Brain, Florian Schanda	A Lightweight Technique for Distributed and Incremental Program Verification.	VSTTE	2012	DBLP DOI BibTeX RDF
1	Jean-Christophe Filliâtre	Verifying Two Lines of C with Why3: An Exercise in Program Verification.	VSTTE	2012	DBLP DOI BibTeX RDF
1	Peter-Michael Osera, Vilhelm Sjöberg, Steve Zdancewic	Dependent interoperability.	PLPV	2012	DBLP DOI BibTeX RDF
1	Alan Jeffrey	LTL types FRP: linear-time temporal logic propositions as types, proofs as functional reactive programs.	PLPV	2012	DBLP DOI BibTeX RDF
1	Manuel Gesell, Klaus Schneider	A hoare calculus for the verification of synchronous languages.	PLPV	2012	DBLP DOI BibTeX RDF
1	Reynald Affeldt, David Nowak, Yutaka Oiwa	Formal network packet processing with minimal fuss: invertible syntax descriptions at work.	PLPV	2012	DBLP DOI BibTeX RDF
1	Garrin Kimmell, Aaron Stump, Harley D. Eades III, Peng Fu, Tim Sheard, Stephanie Weirich, Chris Casinghino, Vilhelm Sjöberg, Nathan Collins, Ki Yung Ahn	Equational reasoning about programs with general recursion and call-by-value semantics.	PLPV	2012	DBLP DOI BibTeX RDF
1	Vladimir Komendantsky	Reflexive toolbox for regular expression matching: verification of functional programs in Coq+Ssreflect.	PLPV	2012	DBLP DOI BibTeX RDF
1	Benjamin C. Pierce	Verification challenges of pervasive information flow.	PLPV	2012	DBLP DOI BibTeX RDF
1	Afshin Amighi, Stefan Blom, Marieke Huisman, Marina Zaharieva-Stojanovski	The VerCors project: setting up basecamp.	PLPV	2012	DBLP DOI BibTeX RDF
1	V. A. Nepomniaschy, Igor S. Anureev, M. M. Atuchin, I. V. Maryasov, A. A. Petrov, Alexey V. Promsky	C program verification in SPECTRUM multilanguage system.	Automatic Control and Computer Sciences	2011	DBLP DOI BibTeX RDF
1	Uri Pincas	Program Verification and Functioning of Operative Computing Revisited: How about Mathematics Engineering?	Minds and Machines	2011	DBLP DOI BibTeX RDF
1	Catherine Meadows	Program Verification and Security.	Encyclopedia of Cryptography and Security (2nd Ed.)	2011	DBLP DOI BibTeX RDF
1	Joxan Jaffar, Jorge A. Navas, Andrew E. Santosa	Unbounded Symbolic Execution for Program Verification.	RV	2011	DBLP DOI BibTeX RDF
1	Bruno Cuervo Parrino, Juan P. Galeotti, Diego Garbervetsky, Marcelo F. Frias	A Dataflow Analysis to Improve SAT-Based Bounded Program Verification.	SEFM	2011	DBLP DOI BibTeX RDF
1	Yoonsik Cheon, Cesar Yeep, Melisa Vela	CleanJava: A Formal Notation for Functional Program Verification.	ITNG	2011	DBLP DOI BibTeX RDF
1	Ranjit Jhala, Wouter Swierstra (eds.)	Proceedings of the 5th ACM Workshop Programming Languages meets Program Verification, PLPV 2011, Austin, TX, USA, January 29, 2011	PLPV	2011	DBLP BibTeX RDF
1	Nassima Aleb, Zahia Tamen	A memetic algorithm for program verification.	EMS	2011	DBLP DOI BibTeX RDF
1	Shengchao Qin, Chenguang Luo, Wei-Ngan Chin, Guanhua He	Automatically Refining Partial Specifications for Program Verification.	FM	2011	DBLP DOI BibTeX RDF
1	Daniel Dietsch, Bernd Westphal, Andreas Podelski	System Verification through Program Verification.	FM	2011	DBLP DOI BibTeX RDF
1	Grigore Rosu, Andrei Stefanescu	Matching logic: a new program verification approach.	ICSE	2011	DBLP DOI BibTeX RDF
1	Meera Sridhar, Kevin W. Hamlen	Flexible in-lined reference monitor certification: challenges and future directions.	PLPV	2011	DBLP DOI BibTeX RDF
1	Gordon Stewart, Andrew W. Appel	Local actions for a curry-style operational semantics.	PLPV	2011	DBLP DOI BibTeX RDF
1	Edwin Brady	IDRIS ---: systems programming meets full dependent types.	PLPV	2011	DBLP DOI BibTeX RDF
1	Johannes Borgström, Juan Chen, Nikhil Swamy	Verifying stateful programs with substructural state and hoare types.	PLPV	2011	DBLP DOI BibTeX RDF
1	Shuvendu K. Lahiri, Shaz Qadeer, David Walker	Linear maps.	PLPV	2011	DBLP DOI BibTeX RDF
1	J. Strother Moore	Reasoning about digital artifacts with ACL2.	PLPV	2011	DBLP DOI BibTeX RDF
1	Derek Bronish, Hampton Smith	Robust, generic, modularly-verified map: a software verification challenge problem.	PLPV	2011	DBLP DOI BibTeX RDF
1	Rui Wang 0010, Shuo Chen, XiaoFeng Wang, Shaz Qadeer	How to Shop for Free Online - Security Analysis of Cashier-as-a-Service Based Web Stores.	IEEE Symposium on Security and Privacy	2011	DBLP DOI BibTeX RDF	Cashier-as-a-Service, logic bug, program verification, web API, e-Commerce security
1	Zhaopeng Li, Yang Zhang, Yiyun Chen	A Method to Generate Verification Condition Generator.	TASE	2011	DBLP DOI BibTeX RDF	Action Function, Program Verification, Hoare Logic, Verification Condition
1	Lee Hively, Frederick T. Sheldon, Anna Cinzia Squicciarini	Toward Scalable Trustworthy Computing Using the Human-Physiology-Immunity Metaphor.	IEEE Security & Privacy	2011	DBLP DOI BibTeX RDF	C.2.2 Network Protocols, trust establishment system, acces control models, K.6.5.a Authentication, K.6.5 Security and Protection, D.4.6.a Access controls, A.1 Introductory and Survey, C.2.0.f Network-level security and protection, C.4.f Reliability, D.2.15 Software and System Safety, Security, Software Engineering, Reliability, formal methods, Validation, Dependability, negotiations, peer to peer system, Statistical Methods, Testing strategies, Requirements/Specifications, availability and serviceability, Software/Program Verification
1	Thomas L. Clune, Richard Rood	Software Testing and Verification in Climate Model Development.	IEEE Software	2011	DBLP DOI BibTeX RDF	software engineering, program verification, testing strategies, testing and debugging
1	Wihem Arsac, Luca Compagna, Samuel Paul Kaluvuri, Serena Elisa Ponta	Security validation tool for business processes.	SACMAT	2011	DBLP DOI BibTeX RDF