Create accountLogin

Recent searches

No recent searches

Search options

Only available when logged in.
dmv.community is one of the many independent Mastodon servers you can use to participate in the fediverse.
A small regional Mastodon instance for those in the DC, Maryland, and Virginia areas. Local news, commentary, and conversation.

Administered by:

Server stats:

175
active users

dmv.community: AboutStatusProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.3.4

#formalmethods

1 post1 participant0 posts today
Public
screwlisp

#formalMethods #gamedev #programming #commonLisp #acl2 #itch lispy-gopher-show.itch.io/lisp

Since yesterday I advocated strong use of defgeneric, defmethod and McCLIM's define-command, here I present

just giving lisp's defun to acl2's first order #logic.

I present a batch processing style for using acl2 both in #shell and in #lisp with a worked example.

Thoughts and opinions, gamedevs and logical types?

itch.io(formal) game logic - lispmoo2 by screwtape1. Intro This begins part 2 of https://lispy-gopher-show.itch.io/lispmoo2/devlog/906389/my-programming-principles-for-game-dev-12 . Which contains the first five parts. These second five parts contain...
Public
Andrew Helwer

Reading the new experience report paper "System Correctness Practices at AWS" by @marcbrooker & Ankush Desai, a successor to 2015 paper "How Amazon Web Services Uses Formal Methods". Documents a whole buffet of industrial formal methods use: P (including new tool PObserve for runtime trace validation), deterministic simulation testing in Rust with the open-sourced Shuttle and Turmoil tools, Dafny, HOL Light, and the open-sourced Kani model-checker for Rust.

While TLA⁺ was the most prominent featured tool in the 2015 paper, it's been lost in the crowd here as part of a clear shift toward verifying & testing the actual running code. I think TLA⁺ must carve out a niche for itself in a world where deterministic simulation testing becomes a commodity technology, or it risks losing relevance same as other design-level tools like UML. There are existing case studies on using TLA⁺ for trace validation and model-driven testing, but a lot of effort needs to go into tooling for making such integrations as smooth as possible instead of bespoke one-off projects.

dl.acm.org/doi/10.1145/3712057

QueueSystems Correctness Practices at AWS: Leveraging Formal and Semi-formal Methods: Queue: Vol 22, No 6 Building reliable and secure software requires a range of approaches to reason about systems correctness. Alongside industry-standard testing methods (such as unit and integration testing), AWS has adopted model checking, fuzzing, property-based testing, ...
#TLAplus#FormalMethods
Public
Jan de Muijnck-Hughes

I have a funded #PhD position for UK students, available with myself and @bentnib

This project will be looking at developing new methods for asserting the resilience of existing communicating systems by developing new static analysis methods derived from advanced programming language research.

Deadline: Thursday 20th March 2025

You will belong to @StrathCyber and @mspstrath, as well as gaining access to @spli

For now more details about the project are on my personal website.

tyde.systems/page/position/202

Please spread the words.

Jan de Muijnck-HughesTowards Type-Driven Assurance of Communicating SystemsDeadline Thursday 20 March 2025 Duration 36 Months Start Date October 2025 Funding Home fee, Stipend Supervisors Jan de Muijnck-Hughes, Bob Atkey Groups StrathCyber, MSP This JARSS PhD studentship will develop new methods for asserting the resilience of existing communicating systems by developing new static analysis methods derived from advanced programming language research as pioneered by the supervising team, and the wider MSP and StrathCyber research groups. Contact Informal enquiries about the studentship are to be directed to Jan de Muijnck-Hughes (Jan.
#dependentTypes#formalMethods#idris
Public *
Reid D. M.

Okay here's an oddly specifc #devops meets #sre and #fp / #formalmethods problem.

I've got a lockfile/solution of package versions. I've also got a set of other versions of the same packages including in some sense known bad versions (CVEs) and a test suite which with some confidence will pass if an upgrade is good.

I want to use (non)dependencies between packages to split upgrade groups (we can upgrade these without those) and plan a sequence of upgrade steps.

Know any prior art?

Public
B W Bush

#introduction

I am a #physicist who has focused much of my career on the #modeling, #simulation, #visualization, and #analysis of #complexSystems (especially #infrastructure and #renewableEnergy), and who is currently working on the #Cardano #blockchain. I love #functionalProgramming, #Haskell, #formalMethods, #categoryTheory, #datavis, #infovis, #XR, #statistics, and teaching.

I have passion for art, music, language, and #meditation; I occasionally create #painting, #sculpture, and #poetry.

ExploreLive feeds
About