A Beginner's Guide to Formalization in Software Engineering
A reading guide for students who want to make sense of the definitions, notation, and rules in program analysis papers.
Learning to read formal definitions takes practice. You learn to identify the objects a paper is talking about, follow the rules that change a program’s state, and work out what an analysis actually guarantees. With so many unfamiliar ideas, deciding where to begin can be as difficult as understanding any particular definition.
This guide helps you choose a route through the series. The first six articles form the main sequence: notation and program states lead into semantics and abstraction, then into an analysis algorithm. The later articles examine soundness, engineering trade-offs, and the questions raised by AI-generated code. Part 7 steps back from the technical material to trace the history of these ideas.
Read the series in order, or go straight to a topic you need for a paper. Each card below describes the question its article addresses. The suggested routes help you choose where to begin.
You do not need to finish all seven articles in one go. Start with the question that is holding up your reading, then return to the surrounding ideas when you need them.
The seven articles
All seven articles are available in English and Chinese. Use the language switch at the top of each page to move between versions.
Reading the Notation: Sets, Mappings, and Program States
Start with common symbols and learn to read formal definitions in terms of familiar programming concepts.
Where Can a Program Go? From Code and CFGs to Program Semantics
Follow the possible paths through a program and see how its state changes along the way.
Keeping What Matters: From Concrete States to Abstract Interpretation
See why an analyzer has to forget some details, and how it can still preserve the properties we care about.
Why Does the Analyzer Stop? Transfer Functions and Fixed Points
Follow information as it moves through a program, and see how the analysis of a loop reaches a stable result.
Precision, Speed, and Soundness: Engineering Trade-offs in Static Analysis
Connect the definitions to real tools: what does an analysis promise, and what does it give up?
AI Wrote the Code. Who Checks It?
Examine what tests, analyses, and proofs can tell us about code generated by a model.
A Short History: From “What Is Computation?” to “Can We Trust This Program?”
Look back at the problems that led people to develop the formal methods we use today.
Choosing a reading route
Choose a route that fits what you want to learn.
Read Parts 1–6 in order, then turn to the history article to see how these ideas developed.
Start with Parts 1 and 2, then jump to the topic that is giving you trouble.
Go straight to Part 7. It introduces the ideas in their historical context and can be read on its own.
The aim is to give you somewhere to start the next time you meet an unfamiliar formula. Rather than skipping the whole passage, you can look for its objects, the relationships between them, and the rules that operate on them. Each article gives you practice with a different part of that reading process.