STRANGER (STRing AutomatoN GEneratoR) performs symbolic string verification on PHP programs. The technical features include that: (1) we encode the set of string values that string variables can take as automata. (2) we implement all string functions using a symbolic automata representation (MBDD representation from the MONA automata package) and leverage efficient manipulations on MBDDs, e.g., determinization and minimization. (3) we propose a novel algorithm for language-based replacement. This replacement function takes three DFAs as arguments and outputs a DFA. (4) we apply a widening operator defined on automata to approximate fixpoint computations. [SPIN2008]
We propose a novel method for modular verification of BPEL service composition. We first use symbolic fixpoint computation to derive relations of the incoming and outgoing messages for well-defined web services based on reachability analysis. The relations are collected and serve as a repository of summarizations of individual web services. We then compose the summarization of external invocations, resulting in scalable verification of web service composition. We realize our ideas in VeriBPEL. The technical features include (1) a novel symbolic encoding for modeling the concurrency semantics of systems having both internal multi-threading and external message passing, and (2) a method for summarizing concurrently running processes, along with a modular verification framework that utilizes these summaries for scalable verification.
In this project, we propose size abstraction and size analysis to verify specifications of object oriented models based on infinite state model checking techniques. We conducted a case study on Java Card API OCL specifications. We revealed various bugs in 26 out of the 150 method specifications, as well as provided fully verified ones. [ESEC/FSE2007]
Neurons are arguably one of the most interesting cell-types in the human body. A large number of neurons working in a cooperative manner are able to perform tasks that are not yet matched by the tools we can build with our current technology. Spiking Neuron P-systems (SNPs) incorporate ideas from spiking neurons into membrane computing. In this project, we give characterizations of sets definable by partially blind multicounter machines in terms of k-output SNPs operating in a sequential mode. [UC2006] [NC2008]
SATRepair is an efficient SAT-based tool to solve Spare Allocation Problem (SAP). By investigating a novel Boolean encoding, we reduce SAP to a Boolean Satisfiability problem (SAT), and take advantage of modern SAT solvers to solve SAP efficiently. We claim that the nature of SAP, i.e., finding a solution, makes it ideal for SAT application. We further implement a test-generator based on realistic fault models and report the simulation results of experiments comparing against BDDRepair and other algorithms found in literature. [DFT2005]
In this project we develop a new SAT-based model checker, named xBMC, to solve the reachability problem of real-time systems. In xBMC, we encode the behavior of region automata as Boolean formulas, and efficiently represent region graph via discrete interpretations. To support both property refutation and verification, we also incorporate inductive methods in xBMC. Once the inductive proof is constructed, one can prove the correctness of the system without reaching the intrinsic threshold, i.e., the number of regions. [FORMATS/FTRTFT2004][ATVA2004][IJFCS2006]
WebSSARI stands for Web application Security via Static Analysis and Runtime Inspection. Viewing Web application vulnerabilities as a secure information flow problem, we created a lattice-based static analysis algorithm derived from type systems and typestate, and addressed its soundness. We applied both the typestate-based polynomial-time algorithm and bounded model checking (BMC) for verifying Web application code. Vulnerable sections of code are patched automatically with runtime guards, allowing both verification and assurance to occur without user intervention. Model checking techniques have relatively complexity, but they provide counterexamples, precise models, and significantly reduce the false positive rate.[WWW2004][DSN2004]
Coworker: Geng-Dian Huang
RED is a full TCTL symbolic simulator/model checker for real-time systems, which was initiated by Prof. Farn Wang since 1996. Due to its novel representation (Clock Restriction Diagrams), RED has shown some promise to perform verification against various benchmarks and industrial protocols. In this project, we focused on developing the following features of RED 4.0: symbolic simulation, numerical coverage estimation, greatest fixed point computation, and pointer data structure analysis. [RTCSA2003][CIAA2003][FORTE2003][TSE2004][TSE2006]
TimeC is an expanding C language supporting timing behavior, e.g., duration, switch-event, and temporal assertions via Open Verification Language (OVL). Using TimeC , engineers can model timing behavior and claim temporal assertions in C programs seamlessly. We develop an optimized translator to translate timed programs to timed automata, and temporal assertions to TCTL formula in the input format of RED, so that we can automatically verify TimeC programs against their OVL assrtions via the symbolic TCTL model checker.[RTCSA2003][JEC2004]