~lobsters | Bookmarks (16)

clear filters

formalmethods ×

Don't let Alloy facts make your specs a fiction

hillelwayne.com

I’ve recently done a lot of work in Alloy and it’s got me thinking about a...
I’ve recently done a lot of work in Alloy and it’s got me thinking about a common specification pitfall. Everything in the main post applies to all formal specifications, everything in dropdowns is for experienced Alloy users. Consider a simple model of a dependency tree. We have a set of top-level dependencies for ...

alloy formal methods formalmethods
1
Release 0.4.0 of the seL4 Device Driver Framework - Devel - lists.sel4.systems

sel4.systems

formalmethods osdev performance security
2
On Invariance and Inconsistency

hansdieterhiep.nl

How can you explain important concepts from program correctness in a simple and intuitive manner? In...
How can you explain important concepts from program correctness in a simple and intuitive manner? In this blog post, we shall have a look at some puzzles and analyze them from the perspective of program correctness. This way we can nicely explain and demonstrate the usefulness of two important concepts, namely invar...

formalmethods teaching
1
Refactoring With Proofs | Craft vs Cruft 36

youtube.com

formalmethods science & technology testing video
1
Co-Developing Programs and Their Proof of Correctness

acm.org

Credit: Balein / Shutterstock Twenty years ago, Sir Tony Hoare proposed a grand challenge to the...
Credit: Balein / Shutterstock Twenty years ago, Sir Tony Hoare proposed a grand challenge to the computing research community: to develop a verifying compiler [which] uses mathematical and logical reasoning to check the correctness of the programs that it compiles. Hoare went on to set demanding success criteria for...

formalmethods programming
1
Lisp Ireland, February 2024 Meetup - Lisp & Hardware Verification with ACL2

youtube.com

formalmethods hardware lisp science & technology video
1
Jesper Cockx - 6 Reasons in favor of a core language, and 5 against

jesper.cx

formalmethods
1
ceps/text/069-coq-roadmap.md at coq-roadmap · coq/ceps

github.com

formalmethods
1
Lamport clocks

fponzi.me

distributed distsys formalmethods paper tla+
2
The Ur Programming Language Family

impredicative.com

formalmethods
2
Verifying using temporal logic of action in Dafny

rdivyanshu.github.io

formalmethods
1
Formalizing Date Arithmetic and Statically Detecting Ambiguities for the Law

rmonat.fr

Abstract: Legal expert systems routinely rely on date computations to determine the eligibility of a citizen...
Abstract: Legal expert systems routinely rely on date computations to determine the eligibility of a citizen to social benefits or whether an application has been filed on time. Unfortunately, date arithmetic exhibits many corner cases, which are handled differently from one library to the other, making faithfully transcribing the law into code error-prone, and possibly leading to heavy financial and legal consequences for users....

formalmethods law pdf plt
1
A Modern Compiler for the French Tax Code

arxiv.org

Abstract: In France, income tax is computed from taxpayers’ individual returns, using an algorithm that is...
Abstract: In France, income tax is computed from taxpayers’ individual returns, using an algorithm that is authored, designed and maintained by the French Public Finances Directorate (DGFiP). This algorithm relies on a legacy custom language and compiler originally designed in 1990, which unlike French wine, did not age well with time. Owing to the shortcomings of the input language and the technical limitations of...

compilers formalmethods pdf plt
1
The World and the Machine

hillelwayne.com

This is just a way of thinking about formal specification that I find really useful. The...
This is just a way of thinking about formal specification that I find really useful. The terms originally come from Michael Jackson’s Software Requirements and Specifications. In specification, the machine is the part of the system you have direct control over and the world is all the parts that you don’t. Take a si...

formal methods formalmethods terms theorycrafting
2
A Beginner's Companion to Theorem Proving in Lean 4 | Blog | emallson.net

emallson.net

formalmethods
2
GitHub - informalsystems/quint: An executable specification language with delightful tooling based on the temporal logic of actions (TLA)

github.com

formalmethods programming
2

~lobsters | Bookmarks (16)

Tags

Domains

Don't let Alloy facts make your specs a fiction

Release 0.4.0 of the seL4 Device Driver Framework - Devel - lists.sel4.systems

On Invariance and Inconsistency

Refactoring With Proofs | Craft vs Cruft 36

Co-Developing Programs and Their Proof of Correctness

Lisp Ireland, February 2024 Meetup - Lisp & Hardware Verification with ACL2

Jesper Cockx - 6 Reasons in favor of a core language, and 5 against

ceps/text/069-coq-roadmap.md at coq-roadmap · coq/ceps

Lamport clocks

The Ur Programming Language Family

Verifying using temporal logic of action in Dafny

Formalizing Date Arithmetic and Statically Detecting Ambiguities for the Law

A Modern Compiler for the French Tax Code

The World and the Machine

A Beginner's Companion to Theorem Proving in Lean 4 | Blog | emallson.net

GitHub - informalsystems/quint: An executable specification language with delightful tooling based on the temporal logic of actions (TLA)