Sérgio Vale Aguiar Campos

Esta página em português

Research Interests

  • Find out what it is.
  • See how it works in practice.
  • Read more about it.
  • Other references

    • Automatic Verification of Distributed and Real-Time Systems

    Techniques for automatic verification and their applications to practical problems. Verification and analysis of distributed and real-time systems.

    The task of verifying if a computing system satisfies its specifications is extremely important. Such systems are frequently used in aplications where failures can have very serious consequences. My work proposes an efficient method to perform this task. The method is based on temporal logic model checking, a technique for verifying reactive systems. In the method proposed a real-time system is represented by a finite state transition graph implemented using binary decision diagrams (BDDs). Efficient symbolic algorithms explore the graph in order to determine if the system satisfies or not its specifications.
    This technique has been used in the verification of various systems of industrial complexity such as aircraft controllers, robotics systems and the PCI local bus, demonstrating that the method proposed can be used to help solving practical problems.

    Verus - A Compiler/Verifier for Real-Time Systems

    To find out more about Verus, check out the (short) paper:

    S. Campos, E. Clarke and M. Minea. The Verus tool: a quantitative approach to the formal verification of real-time systems. In: Conference on Computer Aided Verification, 1997.
    Postscript

    You can install Verus and see for yourself all its advantages (and disadvantages):

  • Verus: verus0.9.tar.gz (92K)
  • BDD library: bddlib.tar.gz (100K)
    • Observations:
  • The code runs without changes in linux, but modifications for unix variants are simple.
  • It is necessary to install the BDD library before installing Verus.
  • Manuals, license agreement, examples and all else is found in the code.

    • Papers

  • S. Campos and E. Clarke, The Verus language: representing time efficiently with BDDs. Fourth AMAST Workshop on Real-Time Systems, Concurrent, and Distributed Software, 1997.
    Abstract , Postscript

  • S. Campos, E. Clarke and M. Minea. Symbolic techniques for formally verifying industrial systems. In: Science of Computer Programming, special issue on Industrially Relevant Applications of Formal Analysis Techniques, 29, pp. 79-98, Elsevier Science, 1997.
    Abstract , Postscript

  • S. Campos, E. Clarke and M. Minea. The Verus tool: a quantitative approach to the formal verification of real-time systems. In: Conference on Computer Aided Verification, 1997.
    Postscript

  • S. V. Campos, E. M. Clarke, W. Marrero and M. Minea. Verifying the performance of the PCI local bus using symbolic techniques. In: International Conference on Computer Design, 1995.
    Abstract , Postscript

  • S. Campos, E. Clarke, W. Marrero and M. Minea, Verus: a tool for quantitative analysis of finite-state real-time systems. In: Workshop on Languages, Compilers and Tools for Real-Time Systems, 1995.
    Abstract , Postscript

  • S. Campos, E. Clarke, W. Marrero, M. Minea and H. Hiraishi, Computing quantitative characteristics of finite-state real-time systems. In IEEE Real-Time Systems Symposium, 1994.
    Abstract , Postscript
  • S. Campos. A Quantitative Approach to the Formal Verification of Real-Time Systems. Ph.D. Thesis, SCS, Carnegie Mellon University, 1996.
    Postscript

    • For more information, a good reference is:

    Carnegie Mellon's model checking project home page

    Back to the main page