Create accountLogin

Recent searches

No recent searches

Search options

Only available when logged in.
med-mastodon.com is one of the many independent Mastodon servers you can use to participate in the fediverse.
Medical community on Mastodon

Administered by:

Server stats:

338
active users

med-mastodon.com: AboutProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.3.8

#formalmethods

0 posts0 participants0 posts today
Public
harryprayiv

If you’re a #haskell user or a proponent of #functionalprogramming please consider donating to the #Purescript project to keep it alive.

It’s a fairly obscure project but, IMO, it is THE language for web #frontend.

On top of that, the backend was recently rewritten in #ChezScheme which tends to be very popular choice in the #formalmethods world due to its rigor.

I see #ghcjs nipping at its heels but IMO, PS will always be a more bespoke and opinionated tool.

opencollective.com/purescript/

opencollective.comContribute - Open Collective
Public
Jan de Muijnck-Hughes

*Last Call*

I have a #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.

*Hard Deadline*: Wednesday 16th April 2025

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

strath.ac.uk/studywithus/postg

(Ignore the deadline on the advert)

Please spread the words.

www.strath.ac.ukTowards Type-Driven Assurance of Communicating Systems | University of Strathclyde
#dependentTypes#formalMethods#idris
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 *
Alley Stoughton

From August 11-14 we're going to be holding a UC (Universally Composable Security)/EasyUC Summer School at Boston University.

Here is a preliminary announcement:

alleystoughton.us/UC-EasyUC-su

If you might be interested in participating in the summer school, we hope you will put yourself on our mailing list and give us feedback that will help us fine tune our plans for the school.

You can also email the organizers at

uc-easyuc-summer-school+owners@googlegroups.com

#UC#Cryptography#FormalMethods
ExploreLive feeds
About