David Harel - researchr profile publications

researchr

You are not signed in
Sign in
Sign up

[Clear Filters]

Publications tagged program verification

The RISC ProofNavigator: a proving assistant for program verification in the classroomWolfgang Schreiner. fac, 21(3):277-291, 2009. [doi]

A Basis for Verifying Multi-threaded ProgramsK. Rustan M. Leino, Peter Müller. ESOP 2009: 378-393 [doi]

Verification of Fine-grain Concurrent ProgramsTony Hoare. ENTCS, 209:165-171, 2008. [doi]

Expander2: Program Verification Between Interaction and AutomationPeter Padawitz. ENTCS, 177:35-57, 2007. [doi]

Programmed Strategies for Program VerificationRichard B. Kieburtz. ENTCS, 174(10):3-38, 2007. [doi]

The Nuggetizer: Abstracting Away Higher-Orderness for Program VerificationParitosh Shroff, Christian Skalka, Scott F. Smith. aplas 2007: 2-18 [doi]

The Why/Krakatoa/Caduceus Platform for Deductive Program VerificationJean-Christophe Filliâtre, Claude Marché. cav 2007: 173-177 [doi]

Playing with Verification, Planning and Aspects: Unusual Methods for Running Scenario-Based ProgramsDavid Harel. cav 2006: 3-4 [doi]

Using Satisfiability Modulo Theories for Inductive Verification of Lustre ProgramsAnders Franzén. ENTCS, 144(1):19-33, 2006. [doi]

Verification of Procedural ProgramsAmir Pnueli. BIRTHDAY 2005: 543-590

A Perspective on Program VerificationWillem-Paul de Roever. vstte 2008: 470-477 [doi]

Verifying the Incorrectness of Programs and AutomataScot Anderson, Peter Z. Revesz. sara 2005: 1-13 [doi]

The Importance of Non-theorems and Counterexamples in Program VerificationGraham Steel. vstte 2008: 491-495 [doi]

Abstracting Call-Stacks for Interprocedural Verification of Imperative ProgramsBertrand Jeannet, Wendelin Serwe. amast 2004: 258-273 [doi]

Verifying Programs that Manipulate Pointers: (Invited Talk)Anders Møller. ENTCS, 98:3-4, 2004. [doi]

Advanced Program Analyses and VerificationsThi Viet Nga Nguyen, François Irigoin. rivf 2003: 77-82 [doi]

ESP: Path-Sensitive Program Verification in Polynomial TimeManuvir Das, Sorin Lerner, Mark Seigle. PLDI 2002: 57-68 [doi]

JavaCard Program VerificationBart Jacobs. tphol 2001: 1-3 [doi]

Verification of Erlang Programs using Abstract Interpretation and Model MheckingFrank Huch. ICFP 1999: 261-272 [doi]

Formal Verification of Concurrent Programs Using the Larch ProverBoutheina Chetali. TSE, 24(1):46-62, 1998. [doi]

On Constructing a Tool to Verify Programs for Processors Built in MachinesT. Ohta, N. Matsumara, Y. Itoh. CSMR 1998: 52-59 [doi]

Formally Specifying and Mechanically Verifying Programs for the Motorola Complex Arithmetic Processor DSPBishop Brock, Warren A. Hunt Jr.. iccd 1997: 31-36

Verifying Programs in the Calculus of Inductive ConstructionsCatherine Parent-Vigouroux. fac, 9(5-6):484-517, 1997.

Syntactic and Semantic Dependence of Array-Arithmetic Sentences, with an Application to Program VerificationLeo Marcus. FUIN, 27(1):77-100, 1996.

Modular Verification for Shared-Variable Concurrent ProgramsJürgen Dingel. concur 1996: 703-718

Hybrid cc, Hybrid Automata and Program VerificationVineet Gupta, Radha Jagadeesan, Vijay A. Saraswat. hybrid 1996: 52-63

Safety Property Verification of ESTEREL Programs and Applications to Telecommunications SoftwareLalita Jategaonkar Jagadeesan, Carlos Puchol, James Von Olnhausen. cav 1995: 127-140

Conditional Lambda-Theories and the Verification of Static Properties of ProgramsMitchell Wand, Zheng-Yu Wang. iandc, 113(2):253-277, September 1994.

Program Verification using HOL-UNITYFlemming Andersen, Kim Dam Petersen, Jimmi S. Pettersson. tphol 1994: 1-15

A Tool for Symbolic Program Verification and AbstrationSusanne Graf, Claire Loiseaux. cav 1993: 71-84

Mechanizing Program Verification in HOLSten Agerholm. tphol 1992: 208-222

Capsules and Types in Fresco: Program Verification in SmalltalkAlan Wills. ECOOP 1991: 59-76 [doi]

Formal Verification of Ada ProgramsDavid Guaspari, Carla Marceau, Wolfgang Polak. TSE, 16(9):1058-1075, 1990. [doi]

Conditional Lambda-Theories and the Verification of Static Properties of ProgramsMitchell Wand, Zheng-Yu Wang. lics 1990: 321-332

Using Symbolic Execution for Verification of Ada Tasking ProgramsLaura K. Dillon. TOPLAS, 12(4):643-669, 1990. [doi]

Verifying General Safety Properties of Ada Tasking ProgramsLaura K. Dillon. TSE, 16(1):51-63, 1990. [doi]

Lawful Functions and Program Verification in MirandaSimon J. Thompson. SCP, 13(1):181-218, 1989.

Strengths and Weaknesses of Program Verification SystemsDan Craigen. ESEC/FSE 1987: 396-404

Specification and Verification of Concurrent Programs By Forall-AutomataZohar Manna, Amir Pnueli. POPL 1987: 1-12

Integration of Program Construction and Verification: The PROSPECTRA MethodologyBernd Krieg-Brückner. Ada-Europe 1987: 173-194

Program Verification in a Logical Theory of ConstructionsPeter Dybjer. fpca 1985: 334-349

Program VerificationRobert S. Boyer, J. Strother Moore. JAR, 1(1):17-23, 1985.

VERIFY: A Program for Proving Correctness of Digital Hardware DesignsHarry G. Barrow. ai, 24(1-3):437-491, 1984.

An Exercise in Automatic Program VerificationWolfgang Polak. TSE, 5(5):453-458, 1979.

The Problem of Reachability and Verification of ProgramsJ. M. Barzdin. mfcs 1979: 13-25

An Introduction to the Construction and Verification of Alphard ProgramsWilliam A. Wulf, Ralph L. London, Mary Shaw. TSE, 2(4):253-265, 1976.

An Introduction to the Construction and Verification of Alphard Programs (Abstract)William A. Wulf, Ralph L. London, Mary Shaw. ICSE 1976: 390

Induction as the Basis for Program VerificationCharles Reynolds, Raymond T. Yeh. TSE, 2(4):244-252, 1976.

Strong Verification of ProgramsSanat K. Basu, Raymond T. Yeh. TSE, 1(3):339-346, 1975.

An Interactive Program Verification SystemDonald I. Good, Ralph L. London, W. W. Bledsoe. TSE, 1(1):59-67, 1975.

runs on WebDSL