What are some code examples demonstrating KeY’s strength? Details With so many Formal Method tools available, I was wondering where KeY is better than its competition, and how? Some readable code...

Continuing on from ideas in: Are there any provable real-world languages? I don't know about you, but I'm sick of writing code that I can't guarantee. After asking the above question and getting ...

Does Isabelle/HOL proof assistant have any weaknesses and strengths compared to Coq?

Looking at C, C has good support for formal methods that can be used in-code(frama-c, VCC, verifast). C++ doesn't seem to have any comparable as far as I can tell. What formal methods are availabl...

I have been interested in formal methods for some time. I have used formal methods to reason about some very specific sub-areas of a few projects I have been working on. I was never able to convinc...

I came upon the Curry-Howard Isomorphism relatively late in my programming life, and perhaps this contributes to my being utterly fascinated by it. It implies that for every programming concept the...

Traditionally most work with computational logic was either propositional, in which case you used a SAT (boolean satisfiability) solver, or first-order, in which case you used a first-order theorem...

What types of applications have you used model checking for? What model checking tool did you use? How would you summarize your experience w/ the technique, specifically in evaluating its ef...

Is there a tool which can handle model checking large, real-world, mostly-C++, distributed systems, such as KDE? (KDE is a distributed system in the sense that it uses IPC, although typically all ...

When using formal aspects to create some code is there a generic method of determining a loop invariant or will it be completely different depending on the problem?

I'm looking at the requirements for automated software verification, i.e. a program that takes in code (ordinary procedural code written in languages like C and Java), generates a bunch of theorems...

Here's a sort of odd question. I'm in the process of writing a book on learning to program using formal methods, and I'm going to target it toward people with some programming experience. The...

Our client wants us to build a web-based, rich internet application for gathering software requirements. Basically it's a web-based case tool that follows a specific process for getting requi...

I'm trying to (classically) prove ~ (forall t : U, phi) -> exists t: U, ~phi in Coq. What I'm trying to do is prove it contrapositively: 1. Assume there is no such t (so ~(exists t: U, ~phi...

So... I teach formal methods in software engineering. I also teach "agile methodologies". Most people seem to think this is contradictory. I think it makes a lot of sense... I also work for ...