15K subscribers • 68 videos on Hallway
Beginner. No background in the topic needed.
10K views4 years ago1 recommendation
Computer scienceSoftware designFormal methods and verificationComputation and complexity
Jeff Weiss introduces TLA+ by modeling a state machine and using the model checker to prove correctness and liveness.
This video was recorded at Code BEAM V 2020 - codesync.global/conferences/code-beam-sto/ A Beginner's Guide to TLA+ Exploring State Machines & Proving Correctness | Jeff Weiss - Senior Software Engineer at Enbala Power Networks ABSTRACT TALK LEVEL: BEGINNER / INTERMEDIATE / ADVANCED This talk introduces TLA+ by taking a small package from hex, examining its properties, modeling its behaviour as a state machine, creating TLA+ correctness and liveness specifications for it, and then using the TLA+ model checker to prove correctness. No prior exposure to formal methods like TLA+ or PlusCalc are necessary. A passing familiarity with state machines is recommended, but not required. OBJECTIVES Introduce TLA+ and its value Illustrate conversion of a state machine to a TLA+ specification Building and checking correctness and liveness models of that TLA+ specification TARGET AUDIENCE Developers interested in adding more rigour to their problem solving and more quickly surfacing design errors. • Follow us on social: Twitter: twitter.com/CodeBEAMio LinkedIn: linkedin.com/company/27159258 • Looking for a unique learning experience? Attend the next Code Sync conference near you! See what's coming up at: codesync.global • SUBSCRIBE TO OUR CHANNEL youtube.com/channel/UC47eUBNO8KBH_V8AfowOWOwWhat people say. Recommended as an amazing introduction to adding rigor to problem solving using TLA+ and formal methods.
u/erlangsolutionsin r/elixir • Recommends