2k views

### Program Correctness, The specification

From Wikipedia: In theoretical computer science, correctness of an algorithm is asserted when it is said that the algorithm is correct with respect to a specification. But the problem is that to get ...
675 views

### How often is Prolog/ASP used in non-research areas?

I've just recently found out about KRR (Knowledge representation and Reasoning) and ASP, not hearing a thing about them before (except a bit about prolog). I've read a bit about them and one of their ...
• 211
205 views

### How CompCert "proves" different things in its codebase

In order to understand examples of formal proofs, I am interested in how CompCert applies "proof" techniques. Specifically, I am wondering what a particular example is of something CompCert "proves" ...
• 2,193
1 vote
351 views

### What to prove and how to prove it

In learning about proof theory, I am interested to know how to go about "proving properties of a program". I don't exactly see yet what needs to be proven, nor how to prove it, which leads to this ...
• 2,193
146 views

### High-level requirements for a Proof of "Saving to the Database"

This question is about a few sentence description of what a proof would look like (and technologies / logics involved) for a complex api call through many layers. Trying to get a sense of the ...
• 2,193
1 vote
113 views

### How to prove a side effect in a function

I asked a question earlier about Saving to the Database, which was very general and about the requirements for a proof when you go through many layers of non-verified systems such as the network and ...
• 2,193
1 vote
272 views

### How to use Hoare Logic to Prove this Assertion

Given this assertion in Hoare Logic: \begin{align} &\mathbf{\{p >= 0\}}\\ &s = 0 ; n = 1 ;\\ &\mathtt{while}\ (n <= p)\ \{\\ &\quad s = s + n ;\\ &\quad n = n + 1\\ &\}\\...
• 2,193
255 views

### What you want to "prove" in algorithms

So it seems that you can get pretty far with just type definitions as a formal model of a system. The typed properties verify that the properties will have that type, typed function arguments verify ...
• 2,193
1 vote
188 views

### How to prove $c = a + b$ using Program Verification Techniques

I am trying to prove an elementary thing, but it seems at some point you get down to atoms where you can't prove anything else. This is why I am wondering about proving $c = a + b$, it seems like an ...
• 2,193
1 vote
176 views

### How to apply Hoare Logic to this function

I would like to apply Hoare Logic to realistic, complex imperative programs that use while loops, if statements, functions, modules, etc. and have side effects (e.g. access the network). In order to ...
• 2,193
159 views

### how real example projects apply formal proof techniques

Given that there are examples of formal proofs used to formally verify real-world software applications, I would like to know what these people and teams actually do to create these formal proofs. ...
• 2,193
93 views

### How to apply Operational Semantics to this function

Say I have a function like this: ...
• 2,193