You’re designing a vehicle controller (think: a drone) that must balance against wind.

Requirement:
If the wind intensity stays constant for four consecutive time steps, the controller guarantees that the vehicle returns to the center — as shown in the animation.

How would you design and formalize such a controller?
How would you prove that it satisfies this property?

Read more in our blog post: https://blogic.ink/p/simple-vehicle-controller/

#logic #formalmethods #verification #modelchecking #blog

Prolog for Verification, Analysis and Transformation Tools by M. Leuschel

https://www.semanticscholar.org/paper/Prolog-for-Verification%2C-Analysis-and-Tools-Leuschel/31bce6bb0bfd951718177ebaa77662e135650037

#prolog #modelchecking #formal

I cannot get enough of our shared Vulgar Technobabble that we #ComputerScientists speak. Even #ACM #TuringAward winning blokes speak this way.🤣

Interviewer—What is a good way to understand what #ModelChecking is and what it does?

#AllenEmerson—[staring intently at his toes] Well, uh, in "layman's terms", model checking is an algorithmic method of verifying correctness of nominally finite state systems, uh, against a specification that's typically given in temporal logic. Uh, if the model checker, the model checking tool that's been implemented, uh, returns "yes", then the system is correct. If it, uh, returns "no", the specification is violated, and a counterexample is produced.

Sure, we get it; it is but #SoftwareVerification in so many words. But does a "layman" get it?

https://youtu.be/sUwxA8px7O8?si=O4MVOVDT2rkIToNd

#VulgarLatin https://en.wikipedia.org/wiki/Vulgar_Latin

ESBMC - An Efficient SMT-based Bounded Model Checker

https://ssvlab.github.io/esbmc/

"ESBMC is an open-source, [...], context-bounded model checker based on satisfiability modulo theories for verifying single- and multi-threaded C/C++ programs. It does not require the user to annotate the programs with pre- or postconditions, but allows the user to state additional properties using assert-statements, that are then checked as well."

1/3

#SMT #FormalVerification #FormalMethods #ModelChecking

Master thesis by Michał Raczkiewicz: "Model Checking Under JAM21"

"This thesis presents the first known implementation of a model checker for the Java memory model JAM21 within the GenMC framework - a tool for stateless model checking using custom memory models. [..] We provide a formal proof of equivalence between the new vector clock algorithm and the original implementation to ensure correctness."

https://repository.tudelft.nl/record/uuid:3c4c7d73-b084-4a4d-9d6d-93256bc09598

#Java #ModelChecking #MemoryModels #FormalProofs #master #thesis

Understandable & predictable performance has its benefits!

#FormalMethods #TLAPlus #ModelChecking

The inner magic behind the Z3 theorem prover - Microsoft Research (October 2019):

https://www.microsoft.com/en-us/research/blog/the-inner-magic-behind-the-z3-theorem-prover/

#Z3 #SMT #FormalVerification #ModelChecking #Proof