• PAT is a model checking system for composing, simulating and reasoning of concurrent, real-time and probabilistic systems. It has attracted 3000+ registered users from 800+ organizations in 71 countries, inc: Microsoft, HP, Sony, Hitachi, Canon, Samsung. The PAT verification tool has been used to verify many highly complex concurrent and distributed algorithms and has discovered previously unknown bugs in popular published election protocol algorithm. PAT was also used to find unknown security flaws in the implementations of several real-world web sites (with millions of users) that utilised popular Facebook Connect Protocol and Windows Live Messenger Connect protocols. PAT currently supports 20 different formalisms and languages: from graphical Timed Automata and Timed Process Algebra to programming languages for Sensor Networks, i.e., NesC. Many PAT languages features are based on our early research work TCOZ which is an integrated formalism based Object-Z and Hoare's CSP.
    Read More
  • Filtering constraint networks to reduce search space is one of the main cornerstones of Constraint Programming. In this project, we build on the success of GAC by proposing ways to transform a constraint network into another such that enforcing GAC on the latter is equivalent to enforcing a stronger consistency on the former....
    Read More
  • PowerPointLabs makes creating engaging PowerPoint presentations easy. With PowerPointLab, you can have point-by-point highlights, dynamic transitiion from A to B, in-slide animations...
    Read More
  • In software engineering research, we require benchmarks in order to evaluate and compare novel regression testing, debugging and repair techniques, yet actual regression errors seem unavailable. The most popular error benchmarks, Siemens and SIR, contain mostly manually seeded regression errors. Developers were asked to change the given programs slightly such that they contain errors of varying detectability, i.e., that were more or less difficult to expose. However, in our recent study we find that such seeded regression errors are significantly less complex than actual regression errors, i.e., they require significantly less substantial fixes than actual regression errors. This poses a threat to the validity of studies based on seeded error! We propose CoREBench for the study of complex regression errors.
    Read More