Formal Methods - A usability perspective: Mapping

Author: Prahlad Sampath Affiliation: Development Manager, MathWorks All readers are invited to contribute. You may fill the blog form  here . In my last post I started a discussion about the classic usability book "The Design of Everyday Things" by Don Norman. I talked about the concepts of "Affordances" and "Signifiers". These are the primary mechanism by which users interact with design. Affordances refer to a relationship between an object, the functions it can perform, and the operations that can be performed by a user on it to achieve these functions. Signifiers are part of the design that help users identify the presence of an affordance. Signifiers further indicate to a user "where" a particular user-action is to be performed to achieve a function. I tried to illustrate these concepts with examples illustrating a few key formal methods artifacts ("things").  In this post, I would like to introduce another concept -- M

Pinaka: Symbolic Execution meets Incremental Solving

Author: Prof. Saurabh Joshi Affiliation: CS Dept, IIT Hyderabad All readers are invited to contribute. You may fill the blog form here . Symbolic execution as well as incremental solving has been quite well known concepts to the researchers and students working in the field of Formal Methods. Today I am going to write about Pinaka , a symbolic execution engine that combines symbolic execution with incremental solving in a fairly simple fashion. Incremental Solving Many modern day constraint solvers, such as SAT and SMT solvers support incremental solving in some fashion. Say, for some problem, we require solutions for the following set of formulas: φ , φ ∧ Δ 1 , φ ∧ Δ 1 ∧ Δ 2 \varphi, \varphi \wedge \Delta_1, \varphi \wedge \Delta_1 \wedge \Delta_2 φ , φ ∧ Δ 1 ​ , φ ∧ Δ 1 ​ ∧ Δ 2 ​ One of the ways to solve these is to create a solver instance for each of these formulas separately and ask the solver for a solution for each of th