For good software quality, it is necessary to use techniques that analyze the behavior of the software and detect potential problems and solutions. However, the cost of these tools is high due to the complexity of today’s software systems.
At VRAIN of UPV, we use techniques that help reduce the associated costs, both temporal and in terms of memory, such as abstract interpretation or symbolic or partial representations that have the advantage of being designed to ensure reliability. Therefore, by using these reduction/compaction techniques, VRAIN of UPV is able to mitigate the problem of the high cost (temporal and memory) of tools that analyze and verify the behavior of software systems.
This service is applicable in the optimization of verification tools, debugging tools, static program analysis, and software testing. Its advantages include faster execution of tools and more competitive software analysis and verification applications in terms of response time and reliability. In addition to supporting the improvement of verification techniques, concurrent systems in particular have added complexity when it comes to ensuring their proper behavior due to the interleaving of execution threads. At VRAIN of UPV, we can assist in modeling the critical aspects of concurrent systems to be able to use existing verification tools specific to these systems. We also advise on the use of tools for automatic generation of test cases.