Is this really a refactoring? Automated equivalence checking for Erlang projects
summary
EquivcheckEr compares old and new versions of changed Erlang functions by running them on randomly generated inputs and only reports concrete counterexamples; it captures exceptions, stdout and sent messages by substituting the runtime IO actor and transforming send/receive nodes with a par transform, infers argument types with Typer to pick better generators, integrates with git, is open source on GitHub, found discrepancies in OTP but they were benign, and typically runs in about 10 seconds.
AI-written summary · about
chapters (13)
- 0:00Equivalence checking intro
- 0:23What is refactoring
- 3:14Need for automated verification
- 5:20EquiChecker features
- 7:28Refactoring tool properties
- 8:33Property-based testing
- 11:00Side effects in Erlang
- 13:28Actor context simulation
- 15:56Defining equivalence
- 18:26Test data generation
- 20:36Static analysis limits
- 21:58Tool results
- 23:03Q&A
related talks
26mTowards Efficient Model Comparison Using Automated Program Rewriting
47mTesting the Hard Stuff and Staying Sane
24mSet-Theoretic Type Checking of Beginner Erlang Code: A Retrospective Study
47mThe Tension Between Expediency and Correctness
51mA CutEr Tool
36mTypeCheck Effortless Runtime Type Checking
28mEtna: An Evaluation Platform for Property-Based Testing
33mLets Generate Tests