← Home

Formal Methods & Research

An introductory series on formal methods, from set theory and logic to SAT and SMT solvers, alongside research projects in model checking, control systems, and robotics.

  • Formal Methods 101: Induction
    Article

    Formal Methods 101: Induction

    Introduction: Induction is a mathematical technique used to prove a property of a system. Intuitively, you can think of induction as a way of proving that all…

  • Formal Methods 101: Formal Systems
    Article

    Formal Methods 101: Formal Systems

    Introduction: A Formal System is a set of formulas (axioms, or derived from axioms) that are used to infer properties, theorems, or additional truths. Axioms c…

  • Formal Methods 101: Decidability
    Article

    Formal Methods 101: Decidability

    Introduction: There are some problems for which there does not exist an algorithm that can guarantee to return a correct (ex. yes or no) answer. These are call…

  • Formal Methods 101: Complexity Theory
    Article

    Formal Methods 101: Complexity Theory

    Introduction: Complexity Theory deals with how ‘complex’ a problem is to solve. That is, how many steps it takes to solve a problem. This topic is one of the m…

  • Formal Methods 101: Second-Order (and Higher-Order) Logic
    Article

    Formal Methods 101: Second-Order (and Higher-Order) Logic

    Introduction: Second-Order Logic extends First-Order Logic to Quantify Sets. Whereas first-order logic may only quantify Variables in a domain of discourse (se…

  • Formal Methods 101: Boolean Satisfiability (SAT)
    Article

    Formal Methods 101: Boolean Satisfiability (SAT)

    Introduction: A Boolean-valued logic formula (predicate) is said to be Satisfiable (SAT) if a valid assignment (also known as a model) to the predicate variabl…

  • Formal Methods 101: Satisfiability Modulo Theories (SMT)
    Article

    Formal Methods 101: Satisfiability Modulo Theories (SMT)

    Introduction: The Satisfiability Modulo Theories (SMT) problem is an extension to SAT problems in which the variables take on values beyond just Boolean-valued…

  • Formal Methods 101: Binary Relations
    Article

    Formal Methods 101: Binary Relations

    Introduction: Relations (R) are a generalization of functions (f), (such that f ⊂ R) and are used to specify sets; or more intuitively the relationship between…

  • Formal Methods 101: Zero-Order (Propositional) Logic
    Article

    Formal Methods 101: Zero-Order (Propositional) Logic

    Introduction: Zero-Order Logic (also known as propositional logic or propositional calculus) is the foundation of most formal logic systems. In Zero-Order Logi…

  • Formal Methods 101: First-Order Logic (FOL)
    Article

    Formal Methods 101: First-Order Logic (FOL)

    Introduction: First-Order Logic extends Zero-Order Logic (or Propositional Logic) to include variables and quantifiers. First-Order Logic operators are used to…

  • Formal Methods 101: Set Theory
    Article

    Formal Methods 101: Set Theory

    Introduction: Set Theory involves sets which are unordered lists. Ex. Set: S = (a, b, c) Note: S is the set and a, b, c are the elements of the set. All member…

  • Model-Based Design of a Closed-Loop Speed Controller for a Hybrid System
    Article

    Model-Based Design of a Closed-Loop Speed Controller for a Hybrid System

    Model-Based Design (MBD) has been used for decades to design controllers for hybrid systems. MBD requires special considerations when modeling, designing, and…

    CodePaper
  • Particle Filter Speed Controller for a Closed-Loop Vehicle System
    Article

    Particle Filter Speed Controller for a Closed-Loop Vehicle System

    Particle filters provide an effective stochastic method for predicting an unknown distribution; this makes them suitable for predicting the underlying properti…

    CodePaper
  • Analysis of N-Queens Stochastic Algorithms Using Probabilistic Model Checking
    Article

    Analysis of N-Queens Stochastic Algorithms Using Probabilistic Model Checking

    Probabilistic model checking extends model checking to domains in which actions will be taken based on a certain probability. This aligns nicely with modeling…

    CodePaper
  • WebGME: Railway Network Design Studio
    Article

    WebGME: Railway Network Design Studio

    This is a railway-networks-plugin for WebGME that traverses through the tree structures and saves various information in a .zip artifact.

    Code
  • WebGME: Colored Petri Net Design Studio
    Article

    WebGME: Colored Petri Net Design Studio

    Colored Petri Nets are a directed graph modeling approach utilized to reason about race conditions and deadlocks within concurrent systems. We present a Design…

    CodePaper
  • E-Puck Robot Control And A* Navigation
    Article

    E-Puck Robot Control And A* Navigation

    A common problem in autonomous route planning and controls is to implement efficient motor control, sensor feedback, and route planning algorithms to allow a r…

    CodePaper
  • Computer Vision Security System
    Article

    Computer Vision Security System

    Abstract The use of security systems is becoming more prevalent in this modern age. With the advent of machine learning algorithms, there is a unique opportuni…

    CodeYouTubePaper
  • Aircraft Automated Collision Avoidance
    Article

    Aircraft Automated Collision Avoidance

    Aircraft collision avoidance is a pervasive need in this modern age of flight. We present a 2-D automated collision avoidance flight controller for automated c…

    CodePaper