Abstrac
For good software quality, it is necessary to use techniques that analyze the
software behavior and detect possible problems and solutions. But the cost of these
tools is high due to the complexity of today’s software systems.
At VRAIN of the UPV we use techniques that allow us to reduce the associated cost, temporal and
memory, such as abstract interpretation or symbolic or partial representations that
They have the advantage of being designed to guarantee reliability. Therefore, through the use of
these reduction/compaction techniques, VRAIN from the UPV is capable of mitigating the problem
of the high cost (time and memory) of the tools that analyze and verify the
behavior of software systems.
This service has its application in the optimization of verification tools, tools
debugging, static program analysis and software testing. Its advantages lie in
faster execution of tools and analysis computer applications
and software verification that are more competitive in response time and reliability. Besides of
support the improvement of verification techniques, concurrent systems in particular have
an added complexity when it comes to guaranteeing good behavior due to interlacing
of the execution threads. In VRAIN of the UPV we can assist in the modeling of the aspects
critical of concurrent systems to be able to make use of existing verification tools
specific to these systems. We also advise on the use of generation tools
automatic test cases.