Posts

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 -- Mapping …

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 SolvingMany 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 these separately. Note however, that any assignment/model/interpretation that does not satisfy φ\var…