~lobsters | Bookmarks (22)

clear filters

formalmethods ×

New Foundations is consistent

leanprover-community.github.io

formalmethods
1
CakeML

cakeml.org

compilers formalmethods ml
1
ProVerB — SLEBoK

slebok.github.io

ProVerB is a project aimed at explaining program verification tools to practicing software developers, and at...
ProVerB is a project aimed at explaining program verification tools to practicing software developers, and at helping them to find they way around the available tools, clearly and briefly summarising the main purpose of the tool, its current status, relations to other tools, etc. You can read more about the project ...

formalmethods
1
Forge: A Tool to Teach Formal Methods

brownplt.org

Posted on 21 April 2024. For the past decade we have been studying how best to...
Posted on 21 April 2024. For the past decade we have been studying how best to get students into formal methods (FM). Our focus is not on the 10% or so of students who will automatically gravitate towards it, but on the “other 90%” who don’t view it as a fundamental part of their existence (or of the universe). In p...

formalmethods
2
AIQUAL.80[AM,DBL]1 - www.SailDart.org

saildart.org

ai formalmethods
1
TLA+ Web Explorer

will62794.github.io

Github url with docs is at https://github.com/will62794/tla-web Comments

formalmethods
1
Proofcraft News - 2024

proofcraft.systems

News from other years: 2023 2022 2021 Proofcraft is 3 years old and we’re still having...
News from other years: 2023 2022 2021 Proofcraft is 3 years old and we’re still having fun while building a more verified future! Amongst other things, our third year has seen us deliver the functional correctness proof of sel4 on AArch64, progress on the verification of MCS seL4, receive the ACM Software System Awa...

formalmethods
1
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

~lobsters | Bookmarks (22)

Tags

Domains

New Foundations is consistent

CakeML

ProVerB — SLEBoK

Forge: A Tool to Teach Formal Methods

AIQUAL.80[AM,DBL]1 - www.SailDart.org

TLA+ Web Explorer

Proofcraft News - 2024

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