Research Projects

Faculty

• Tevfik Bultan

Graduate Students

• Constantinos Bartzis
• Tuba Yavuz-Kahveci
• Aysu Betin-Can
• Xiang Fu
• Graham Hughes

Related Tools

Composite Symbolic Library is a symbolic manipulator for automated verification. Action Language is a specification language for reactive systems. These tools are developed based on the results obtained from the research projects below.

Current Projects

PROJECT TITLE: Reliable Concurrent Software Development via Reliable Concurrency Controllers

SUMMARY
Run-time errors in concurrent programs are generally due to wrong usage of synchronization primitives such as monitors. Conventional validation techniques such as testing become ineffective for concurrent programs since the state space increases exponentially with the number of concurrent processes. In recent years there has been considerable progress in automated verification techniques for concurrent systems based on model checking. This project presents a framework for reliable concurrent programming based on interface-based specification and verification of concurrency controllers. Proposed specification and verification techniques for concurrency controllers are modularized by decoupling behavior and interface specifications. The behavior specification is a set of actions (which correspond to methods or procedures) composed of guarded commands. The interface specification is a finite state machine whose transitions represent actions. Concurrency controllers can be designed modularly by composing their interfaces. The proposed approach separates the verification of the concurrency controllers (behavior verification) from the verification of the threads which use them (interface verification). For behavior verification it is possible to use symbolic and infinite-state verification techniques which enables verification of controllers with parameterized constants, unbounded variables and arbitrary number of client threads. For interface verification it is possible to use explicit state program verification techniques which enables verification of arbitrary thread implementations without any restrictions. The correctness of the user threads can be verified using stubs generated from the concurrency controller interfaces which improves the efficiency of the thread verification significantly. It is possible to synthesize efficient Java monitors from the concurrency controller specifications, and the generated implementations preserve the verified properties of the specifications. The proposed framework will be implemented as a set of tools for concurrency controller specification, verification and synthesis.

Related publications:

• Aysu Betin-Can and Tevfik Bultan. "Interface-Based Specification and Verification of Concurrency Controllers." In Proceedings of the Workshop on Software Model Checking (SoftMC 2003).
• Tuba Yavuz-Kahveci and Tevfik Bultan. "Specification, Verification, and Synthesis of Concurrency Control Components." Proceedings of the 2002 ACM/SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2002), pp. 169-179, July 22-24, 2002, Via di Ripette, Rome, Italy.

PROJECT TITLE: Developing Reliable Concurrency-Controllers

SUMMARY
In this project, we use automated verification techniques for developing reliable concurrency-controllers. Concurrency-controllers are software components which are used solely for concurrency control. We propose a modular approach to development of concurrency-controllers which: 1) decouples the behavior and the interface specifications of concurrency-controllers and 2) uses both symbolic and explicit state automated verification techniques by exploiting this separation.

Related publications:

• Aysu Betin-Can and Tevfik Bultan. "Interface-Based Specification and Verification of Concurrency Controllers." In Proceedings of the Workshop on Software Model Checking (SoftMC 2003).
• Tuba Yavuz-Kahveci and Tevfik Bultan. "Specification, Verification, and Synthesis of Concurrency Control Components." Proceedings of the 2002 ACM/SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2002), pp. 169-179, July 22-24, 2002, Via di Ripette, Rome, Italy.

PROJECT TITLE: CAREER: Verifiable Specifications: Tools for Reliable Reactive Software Development

SUMMARY
Developing reliable software for reactive systems is a challenging task. This project focuses on combining and extending the results from two areas which address this problem: 1) specification languages and 2) automated verification methods for reactive systems. Building on the recent results in these areas the goal of this project is to develop verifiable specification languages. This will involve research from two directions: 1) From the verification side the goal is to extend the scope of techniques such as model checking to make them applicable to a wider set of systems. 2) From the specification side the goal is to restrict the specification languages as much as possible (without reducing their ability to specify complex systems) in order to make their automated verification feasible. This project will address both theoretical issues such as complexity and efficiency of model checking techniques, and practical issues such as investigating usability of software specification languages and automated verification techniques in practice.

Related publications:

• Aysu Betin-Can and Tevfik Bultan. "Interface-Based Specification and Verification of Concurrency Controllers." In Proceedings of the Workshop on Software Model Checking (SoftMC 2003).
• Tuba Yavuz-Kahveci and Tevfik Bultan. "Automated Verification of Concurrent Linked Lists with Counters." Proceedings of the 9th International Static Analysis Symposium (SAS 2002). M. V. Hermenegildo, G. Pueble eds., LNCS 2477, pp. 69-84, Springer, Madrid, Spain, September 2002.
• Tuba Yavuz-Kahveci and Tevfik Bultan. "Specification, Verification, and Synthesis of Concurrency Control Components." Proceedings of the 2002 ACM/SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2002), pp. 169-179, July 22-24, 2002, Via di Ripette, Rome, Italy.
• Xiang Fu, Tevfik Bultan, and Jianwen Su. "Formal Verification of E-Services and Workflows." In Proceedings of the Workshop on Web Services, e-Business, and the Semantic Web: Foundations, Models, Architecture, Engineering and Applications (WES 2002). C. Bussler, R. Hull, S. McIlraith, M.E. Orlowska, B. Pernici, and J. Yang, eds., LNCS 2512, pp. 188-202, Springer, Toronto, Canada, May 27-28, 2002.
• Giorgio Delzanno and Tevfik Bultan. "Constraint-based Verification of Client-Server Protocols." Proceedings of the Seventh International Conference on Principles and Practice of Constraint Programming (CP 2001), T. Walsh ed., LNCS 2239, pp. 286-301, Springer, Paphos, Cyprus, December 2001.
• Tevfik Bultan and Tuba Yavuz-Kahveci. "Action Language Verifier." Proceedings of the 16th IEEE International Conference on Automated Software Engineering (ASE 2001), pp. 382-386, Coronado Island, California, November 2001.
• Tevfik Bultan. ``Action Language: A Specification Language for Model Checking Reactive Systems.'' Proceedings of the 22nd International Conference on Software Engineering (ICSE 2000), pp. 335-344, University of Limerick, Ireland, June 2000.
• Tevfik Bultan, Richard Gerber and William Pugh. ``Model Checking Concurrent Systems with Unbounded Integer Variables: Symbolic Representations, Approximations and Experimental Results.'' ACM Transactions on Programming Languages and Systems, Volume 21, Number 4, July 1999, Pages 747-789.
• Tevfik Bultan, Richard Gerber and William Pugh. ``Symbolic Model Checking of Infinite State Systems Using Presburger Arithmetic.'' Proceedings of the 9th International Conference on Computer Aided Verification (CAV '97), Orna Grumberg, ed., LNCS 1254, pp. 400-411, Springer, Haifa, Israel, June 1997.
• Tevfik Bultan, Jeffrey Fischer and Richard Gerber. ``Compositional Verification by Model Checking for Counter-Examples.'' Proceedings of the 1996 ACM/SIGSOFT International Symposium on Software Testing and Analysis (ISSTA '96) , San Diego, California, pp. 224-238, January 1996.

Past Projects

PROJECT TITLE: A Composite Model Checking Toolset for Analyzing Software Systems

SUMMARY
The goal of this project is to investigate a new automated verification technique for analyzing software systems called composite model checking. Model checking is a technique for searching the state space of a system to find out if it satisfies a given property. The success of model checking procedures rely on the efficiency of the data structures used to represent the states of the system. In this project a composite model will be developed for combining multiple type-specific representations so that all variable types can be represented efficiently during the state space search. This way, representations such as Binary Decision Diagrams which are efficient for encoding Boolean variables will be combined with representations such as linear arithmetic constraints which can encode unbounded variables. A set of tools will be implemented to support composite model checking. The layered structure of the toolset will allow other researchers to use it at various levels 1) for testing the effectiveness of new representations; 2) for investigating various model checking strategies such as backward and forward search, partitioning and abstraction; or 3) for analyzing complex software specifications.

Related publications:

• Constantinos Bartzis and Tevfik Bultan. "Efficient Image Computation in Infinite State Model Checking." In Proceedings of the 15th International Conference on Computer Aided Verification (CAV 2003). Warren A. Hunt, Jr. and Fabio Somenzi, eds., LNCS 2725, pp. 249-261, Springer, Boulder, Colarado, July 8-12, 2003.
• Constantinos Bartzis and Tevfik Bultan. "Efficient Symbolic Representations for Arithmetic Constraints in Verification." To appear in the International Journal of Foundations of Computer Science (IJFCS).
• Constantinos Bartzis and Tevfik Bultan. "Construction of Efficient BDDs for Bounded Arithmetic Constraints." In Proceedings of the Ninth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2003), Hubert Garavel and John Hatcliff, eds., LNCS 2619, pp. 394-408, Springer, Warsaw, Poland, April 7-11, 2003.
• Constantinos Bartzis and Tevfik Bultan. "Automata-Based Representations for Arithmetic Constraints in Automated Verification." In Proceedings of the Seventh International Conference on Implementation and Application of Automata (CIAA 2002). Jean-Marc Champarnaud and Denis Maurel, eds., LNCS 2608, pp. 282-288, University of Tours, Tours, France, July 3-5, 2002.
• Tuba Yavuz-Kahveci and Tevfik Bultan. "A Symbolic Manipulator for Automated Verification of Reactive Systems with Heterogeneous Data Types." To appear in the International Journal on Software Tools for Technology Transfer (STTT).
• Tuba Yavuz-Kahveci and Tevfik Bultan. "Heuristics for Efficient Manipulation of Composite Constraints." Proceedings of the 4th International Workshop on Frontiers of Combining Systems (FroCoS 2002), Alessandro Armando, ed., LNAI 2309, pp. 57-71, Springer, Santa Margherita Ligure, Italy, April 8-10, 2002.
• Tuba Yavuz-Kahveci, Murat Tuncer, and Tevfik Bultan. "A Library for Composite Symbolic Representations." Proceedings of the Seventh International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2001), Tiziana Margaria and Wang Yi, eds., LNCS 2031, pp. 52-66, Springer, Genova, Italy, April 2001.
• Tevfik Bultan. ``BDD vs. Constraint-Based Model Checking: An Experimental Evaluation for Asynchronous Concurrent Systems.'' In Proceedings of the Sixth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2000). Susanne Graf and Michael Schwartzbach, eds., LNCS 1785, pp. 441-455, Springer, Berlin, Germany, March 2000.
• Tevfik Bultan, Richard Gerber and Christopher League. ``Composite Model Checking: Verification with Type-Specific Symbolic Representations.'' ACM Transactions on Software Engineering and Methodology. Volume 9, Number 1, Pages 3-50, January 2000.
• Tevfik Bultan. ``A Composite Model Checking Toolset for Analyzing Software Systems.'' ACM SIGSOFT Software Engineering Notes, Volume 25, Number 1, January 2000, Pages 37-38.
• Tevfik Bultan, Richard Gerber and Christopher League. ``Verifying Systems with Integer Constraints and Boolean Predicates: A Composite Approach.'' In Proceedings of the 1998 ACM/SIGSOFT International Symposium on Software Testing and Analysis (ISSTA '98), pp. 113-123, Clearwater Beach, Florida, March 1998.

PROJECT TITLE: Tools and Techniques for Workflow Specifications

SUMMARY
In this project we investigated the specification and verification techniques for workflow specifications. Workflow systems are used for organizing the execution of multiple tasks, typically in support of a business or scientific process. Since workflow systems involve concurrent execution of multiple tasks, the control logic could easily get complicated. We applied automated verification techniques to workflow systems and developed several heuristics to improve the efficiency of the verification task. In particular, we investigated developing automated verification techniques for a workflow language called Vortex developed at Bell Labs. As a case study, we verified properties of a Vortex specification for an automated help system for customers browsing a web store-front.

Related publications:

• Xiang Fu, Tevfik Bultan, and Jianwen Su. "Formal Verification of E-Services and Workflows." In Proceedings of the Workshop on Web Services, e-Business, and the Semantic Web: Foundations, Models, Architecture, Engineering and Applications (WES 2002). C. Bussler, R. Hull, S. McIlraith, M.E. Orlowska, B. Pernici, and J. Yang, eds., LNCS 2512, pp. 188-202, Springer, Toronto, Canada, May 27-28, 2002.
• Xiang Fu, Tevfik Bultan, Richard Hull, and Jianwen Su. "Verification of Vortex Workflows." Proceedings of the Seventh International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2001), Tiziana Margaria and Wang Yi, eds., LNCS 2031, pp. 143-157, Springer, Genova, Italy, April 2001.