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

Master thesis by Pepijn Vunderink: "Program Matching with Semantic Patterns"

"We propose the Dyno pattern language, in which concrete object language syntax can be used to express intuitive semantic patterns of programs. Pattern matching is performed by translating Dyno patterns to μ-calculus formulas and model checking these formulas against models extracted from object programs."

https://repository.tudelft.nl/record/uuid:a18ab135-96b1-417c-b25e-46aa02521896

#thesis #PatternMatching #MuCalculus #ModelChecking #mCRL2

Well, I am stuck and stuck hard on #Ivy. Here's my first toy example: https://gist.github.com/mgritter/17b455a33222e22d2b9627db36c0eaff

I want a system where I provide a left number, then a right number, then update a running sum with the absolute value of their difference.

What I get when I try to state that the sum should be increasing is nonsense models of the numbers like

0:num + 0 = 0
0:num + 1 = 0
1:num + 0 = 0
1:num + 1 = 0

Which is a possible model of the + function, I get it! But I cannot convince Ivy to exclude that model. (I think the model of < may be wrong too, but for some reason it's not including that.)

#ModelChecking

@redmp any thoughts on what I'm doing wrong?

There's now a video up of the talk I gave at this year's seL4 Summit, on the status of UNSW's projects to verify Time Protection and Microkit-based userland OS services for the seL4 microkernel:

https://youtu.be/7wcFx6OTEL4

#sel4summit #seL4 #verification #operatingsystems #microkernel #IsabelleHOL #HOL4 #ITP #modelchecking #formalmethods #formalverification #formal_methods #formal_verification

Okay, I no longer hate all large language models 😉

If I understand correctly here they trained an LLM to not try to solve epistemic logic puzzles by itself, but to translate the problem to the input format of my model checker SMCDEL and then ask that 😎 https://arxiv.org/abs/2404.15515

#modelchecking #llm #logic

Master thesis by Matteo Meluzzi: Model Checking the XMM Memory Model

"we present our design of a model checker algorithm for the XMM memory model called GenMC-XMM [...] GenMC-XMM is the first multi-execution model checker proven to be sound. We evaluated our tool against the state-of-the-art model checking tools for RC11, IMM, and Weakestmo2."

https://repository.tudelft.nl/record/uuid:93937121-ae62-4253-a716-d3c911d85e9c

#ModelChecking #compilers #multiexecution #thesis

A Practical Approach for Model Checking C/C++11 code, http://plrg.eecs.uci.edu/publications/toplas16.pdf.

#testing #safety #ModelChecking #cpp

We have an exciting opportunity for a PostDoc
to work applying formal methods to enterprise systems: We will develop
techniques to detect faults and vulnerabilities in complex business-process-driven systems, contributing to
protecting critical workflows such as manufacturing, or logistics.

Apply until the 18th April 2024:
https://jobs.exeter.ac.uk/hrpr_webrecruitment/wrd/run/etrec179gf.open?WVID=171839ediw&LANG=USA&VACANCY_ID=386422ijTy

#Fedihire #Job #BPMN #BPL #FormalMethods #AcademicChatter #Security #ITP #Z3 #postdoc #unijobs
#ModelChecking #EnterpriseSecurity

Related to the curl vulnerability, does anyone have any current favorite tools for doing things like designing state machines or behavior trees such that the model is amenable to checking and ready to go through some code generation so that it can be consumed by a general purpose PL? #ModelChecking https://mastodon.social/@bagder/111214879350843575

The paper "Simplifying process parameters by unfolding algebraic data types" by Anna Stramaglia, Thomas Neele and yt will be presented at #ictac2023

We describe how algebraic data types can be unfolded to improve the performance of symbolic #modelchecking in #mCRL2.

Abstract: https://easychair.org/smart-program/ICTAC2023/2023-12-08.html#talk:239997

I am listening to the @ttforall podcast with Jimmy Koppel on which parts of CS theory all software engineers should learn about (see also his blog post from 2021 on why programmers should(n't) learn theory). Now I'm curious to learn which parts of "theory" you think are the most useful for a software engineer.

Please boost this so this also finds an audience beyond the types community!

#SoftwareEngineering #Education #TypeTheory #ProgramVerification #AbstractInterpretation #ProofAssistant #HoareLogic #ModelChecking #SMT #OperationalSemantics #CategoryTheory #DomainTheory

Gonna try some TLA+ / PlusCal for a work project again - this time using the command-line, because I found the IDE didn't work well with my desires for automation and version control.

@ParslProject has a task dispatcher and the bit of code which ensures the right number of tasks are on worker nodes always feels quite fragile to me - so I'm going to investigate around that.

#TLA+ #PlusCal #ModelChecking

Mostly, software interfaces are only defined by their signature and without a formal description of the admissible behavior and timing assumptions.

#ComMA provides a family of domain-specific languages that integrate existing techniques from formal behavioral and time modeling and is easily extensible.

https://youtu.be/-bbJTg7pJ-k

#SoftwareEngineering
#Interfaces
#Modelling
#ModelChecking
#CodeGeneration

- #Modelchecking, considers systems that have finite state or may be reduced to finite state by abstraction;

I finally finished a new blog post today: Symbolically finding Cheryl's Birthday with SMCDEL https://malv.in/posts/2019-03-01-symbolically-finding-cheryls-birthday-with-SMCDEL.html #haskell #logic #puzzle #modelchecking