Given a specification, does a program satisfy it?

learn more… | top users | synonyms

3
votes
0answers
87 views

How to determine whether a proof requires “higher-order reasoning techniques”?

The question: Suppose I have a specification of a problem consisting of axioms and a goal (i.e. the associated proof problem is whether the goal is satisfiable given all the axioms). Let us also ...
7
votes
1answer
169 views

Complexity of a graph-rewriting problem

I recently came across the following problem which seems to fall in the context of graph rewriting problems: Input: A graph $G=(V,E)$ with maximum degree 3, an edge $e_0 \in E$ and pairs of graphs $(...
6
votes
1answer
96 views

Confusions about the technique for verifying implementations of linearizable objects in [Herlihy and Wing, 1990]

In Section 4.3.2 entitled "Proof Method" of Herlihy and Wing, "Linearizability: A Correctness Condition for Concurrent Objects", 1990 the authors describe the technique for verifying ...
2
votes
2answers
97 views

Practical example: how to formally verify “file name” implementation from a spec?

Say you have an OS-independent specification for file names. The file names are case sensitive, and let's say can't be more than 200 characters, and can't have : or ...
1
vote
1answer
85 views

Regular safety properties and bad prefixes of $\omega$-regular properties

I have two questions: By starting with a nondeterministic Büchi automaton (NBA) $\mathcal{A}^{\varphi} = (Q, \Sigma, \rightarrow, I, F )$ for an $\omega$-regular property $\varphi$, we can construct ...
9
votes
1answer
558 views

Why is Proof Checker required in Proof Carrying Code

In the classical PLDI'98 paper by Necula, "The design and implementation of a certifying compiler", the high-level verifier uses: VCGen to generate verification conditions (safety predicates) First-...
10
votes
1answer
179 views

Type systems preventing laziness-related memory leaks?

Perhaps the main source of performance problems in Haskell is when a program inadvertently builds up a thunk of unbounded depth - this causes both a memory leak and a potential stack overflow when ...
2
votes
1answer
168 views

Advances in program verification?

While trying to check what is the state of art in formal verification, it seemed to me that there were actually no breakthroughs in decades. For example, here http://www.comp.nus.edu.sg/~hobor/...
12
votes
2answers
874 views

Full Completeness vs Full Abstraction of a program translation

Compiler verification efforts often come down to proving the compiler fully abstract: that it preserves and reflects (contextual) equivalences. Instead of providing full abstraction proofs, some ...
2
votes
0answers
164 views

Conversion technique/tool from temporal logic CTL,CTL* or LTL to μ-calculus

Suppose one wants to use a μ-calculus model checker, but specify things in temporal logics, which is easier (more intuitive). Is there a technique (even better, a tool) that automatically translates ...
3
votes
1answer
106 views

Program transformation using partial functions which preserve partial correctness

Much work has been done demonstrating that certain program transformations preserve particular properties. That is, for any program $P$ which has property $\alpha$, show that $P$ transformed under ...
1
vote
2answers
197 views

Using partial functions to prove correctness

I'm interested in proving that a program (which may or may not terminate) will give the correct answer if it terminates. Given: $P$ is a family of programs, parameterized by a function $f$. Write $...
1
vote
1answer
305 views

Verification: how 'formal' is a tool like Java Modeling Language (JML) compared to certified libraries and model checking?

(note: this is probably a beginner question, and English is not my first language) Recently, I have read a paper that used the “Java Modeling Language” (JML), see for instance: http://www.eecs.ucf....
6
votes
1answer
126 views

Step-indexing: Where to begin?

I am about to begin a verification project (for MIPS) with my professor (I am a senior undergraduate) and have been told that the soundness proof for the program logic we need will probably involve ...
3
votes
3answers
279 views

Can Hoare logic be used when objects are created or deleted?

Hoare logic can be used for proving program correctness (e.g. for deriving correctness statements for the whole program from the statements for the individual commands or constructions; good summary ...
9
votes
2answers
304 views

Original Hoare Logic termination paper

I'm looking for the original paper where Hoare (or someone else I suppose) discusses termination (Total Correctness). Or any other early work on termination for "vanilla" Hoare logic (I suppose by ...
14
votes
9answers
1k views

How to Create Mission Critical Software?

I am self learning formal methods. I heard that formal methods is used (and usually only used) to create mission critical software (such as nuclear reactor controller, aircraft flight controller, ...
6
votes
0answers
143 views

Verified Software Repository

Does anyone know if the verified software repository is still alive? Bar that, are there other repositories out there of verified (or just certified) software? The archive of formal proofs is nice, ...
8
votes
1answer
282 views

Proofs techniques related to Curry–Howard correspondence

I am looking for sources about formalized notion of programs. This seems to be closely related to Curry-Howard correspondence, but one could also track this back to Universal Turing Machines and its ...
8
votes
2answers
259 views

Is there any work done on developing difference-calculus of Turing Machines (or simpler Formal Languages)

I am attempting to develop some notions of a difference-calculus between a notional Ideal Turing Machine conceived by a developer (e.g. whatever is intended by a software developer), call it $M_I$, ...
7
votes
1answer
798 views

How to use induction without Fixpoint definition in Coq?

I want to verify a program written in C. I am using Jessie to translate the (pre/post)conditions of the program to Coq. In Coq I will make a proof. Sometimes I need recursive definitions. ...
8
votes
1answer
355 views

What is the proper role of verification in quantum sampling, simulation, and extended-Church-Turing (E-C-T) testing?

Since no answer was given, a flag has been set requesting that this question be converted to a community wiki. The comments by Aaron Sterling, Sasho Nikolov, and Vor have been synthesized into the ...
7
votes
2answers
387 views

What's the simplest to implement of all decent LTL-to-Buchi translation or other LTL verification algorithms?

I'm writing a toy modelchecker, and I'm at the point where it's time to implement LTL to Buchi automata translation. For a variety of obvious reasons, I wish the algorithm to be simple :) e.g. I want ...
27
votes
4answers
1k views

Relationship between contracts and dependent typing

I've been reading some articles on dependent types and programming contracts. From the majority of what I've read, it seems that contracts are dynamically checked constraints and dependent types are ...
13
votes
6answers
570 views

What are practically computable properties of Labelled Transition Systems?

I found labelled transition systems to be a good model for my application, namely there is a paper about modeling use cases using LTSs. The question is, what can be easily proven about LTSs? I would ...
3
votes
1answer
2k views

What's the difference between an invariant and an “inductive” invariant?

I would like to understand this with an example. Also, are there other kinds of invariants related to these? Thanks!
14
votes
3answers
479 views

How hard is it to reduce termination to partial correctness?

If you are familiar with program verification you are likely to prefer reading the Question before the Background. If you are not familiar with program verification then you may still be able to ...