Tagged Questions

Given a specification, does a program satisfy it?

learn more… | top users | synonyms

0
votes
0answers
48 views

Ample sets for partial order reduction?

I am learning aobut model checking, and I am having some trouble conceptualizing what ample sets are for partial order reduction. I don't fully understand why they need to satisfy these four ...
8
votes
2answers
386 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
114 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
99 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
184 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 ...
0
votes
1answer
207 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: ...
6
votes
1answer
117 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
227 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
279 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 ...
13
votes
9answers
741 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
126 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, ...
7
votes
1answer
252 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
248 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$, ...
6
votes
1answer
523 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. ...
9
votes
0answers
292 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
286 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 ...
22
votes
4answers
811 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 ...
12
votes
6answers
537 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 ...
1
vote
1answer
1k 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
424 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 ...