topics.typ

#import "common.typ": *
#show: template.with(dark: false)

= Formal Methods in Software Engineering

Below is the list of topics in the area of formal methods in software engineering.

You can pick any topic or suggest your own to research and prepare a presentation about.

== Advanced Logics and Theoretical Foundations

- Intuitionistic Logic and Constructive Mathematics
- Linear Logic in Concurrency and Resource Management
- Hoare Logic and Program Verification
- Separation Logic for Memory Safety Verification
- Modal Logic Variants: Epistemic, Deontic, and Doxastic
- Alternating-time Temporal Logic (ATL)
- Temporal Logic Extensions: CTL\*, Probabilistic CTL
- Non-Monotonic Logic in AI Reasoning
- Description Logics and Ontology Engineering

== Theorem Proving and Automation

- Interactive Theorem Provers: Coq, Isabelle/HOL
- Automated Theorem Provers: Vampire and E Prover
- Certifying Algorithms and Proof Witnesses
- Boyer-Moore Theorem Prover
- Prolog

== Verification Techniques and Tools

- SMT Solvers in Industry
- Symbolic Execution
- Concolic Testing
- Abstract Interpretation
- Craig Interpolation in Model Checking
- Bounded Model Checking with SAT
- IC3/PDR in Hardware Verification
- Statistical Model Checking of Stochastic Systems
- Termination Analysis
- Alias Analysis
- Shape Analysis
- Predicate Abstraction in SLAM
- Counterexample-Guided Abstraction Refinement (CEGAR)
- Syntax-Guided Synthesis (SyGuS)

== Specification and Modeling Languages

- Z Notation in Industrial Specifications
- TLA+ for System Design
- Process Calculi: π-Calculus and CSP
- SysML for Model-Based Systems Engineering
- Alloy for Lightweight Formal Methods
- Dafny and Verified Software Development
- SCCharts for Synchronous Systems
- Live Sequence Charts

== Historical and Philosophical Context

- Hilbert's Program
- Gödel's Incompleteness Theorems
- The Curry-Howard Correspondence
- The Fifth Generation Project
- The Verified Software Initiative
- Skolem's Paradox
- Turing Award
- The Ada Language and Defense Projects

== Applications and Case Studies

- seL4: Microkernel Verification
- Ethereum Smart Contract Formal Analysis
- DO-178C
- Intel's Hardware Formal Verification
- CompCert: Formally-Verified C Compiler
- Railway Systems with the B Method
- ProVerif for Cryptographic Protocols
- Rust’s Ownership Model
- Autonomous Vehicle Software Verification
- Medical Device Certification with Formal Methods

== Emerging Trends and Interdisciplinary

- Formal Methods for ML Safety (Fairness, Robustness, Privacy)
- Quantum Program Verification
- IoT Security via Formal Models
- Cyber-Physical Systems with Hybrid Automata
- From Legal Contracts to Formal Specifications
- Biological Systems Modeling with Petri Nets
- Formal Ethics in AI Systems
- RISC-V Formal Specification

== Debates and Methodological Challenges

- Agile Development vs. Formal Methods
- Scalability of Formal Verification
- Human Intuition vs. Automated Proofs
- Open-Source Adoption of Formal Methods
- Testing vs. Formal Verification Trade-offs
- Education Challenges in Formal Methods
- Industry-Academia Collaboration Barriers
- Formal Methods in Legacy Systems
- The Future of FM in Quantum Computing

== Tools and Algorithms

- The DPLL Algorithm Evolution
- Conflict-Driven Clause Learning (CDCL) for SAT
- Binary Decision Diagrams (BDDs) in Model Checking
- Knowledge Compilation Techniques
- The Why3 Platform for Deductive Verification
- KeY System for Java Verification
- ACL2 in Industrial Hardware Verification
- SPIN Model Checker and Promela Language
- NuSMV for Symbolic Model Checking
- ProB for B-Model Animation
- JKind Infinite-State Model Checker

== Educational and Outreach

- Gamifying Formal Methods Learning
- MOOCs on Formal Methods (e.g., Coursera, edX)
- Case Studies in Undergraduate FM Courses
- Formal Methods in Programming Competitions
- The Role of Mathematics in SE Education

== Theoretical Computer Science

- Rice's Theorem and Undecidability
- The Halting Problem in Practice
- Automata Theory in Model Checking
- Denotational Semantics
- Type Theory
- Lambda Calculus
- Category Theory
- Heyting Algebras