4, Nov, 2014 11:30
CISTER, Porto, Portugal

ABSTRACT:
In the context of software development, one of the big challenges that we face is that of providing evidence that the underlying algorithms satisfy some set of specifications that characterize the intended behavior of the system at hand. Today’s practice is essentially focused on performing highly expensive and time consuming testing and simulations, but it is well known that these approaches can miss some cases which may occur upon execution time and lead to undesirable consequences (namely when we consider safety-critical systems). With the goal of tackling the inherent difficulties that are associated with proving the correctness of software, the area of Formal Verification provides us with a gamut of techniques and approaches that allows us to formally prove (at least) that the code that we write is indeed correct according to its (formal) specification. In this talk, we will provide an overview of the mathematical foundations of Formal Verification and present some of the techniques and tools (static and dynamic) that programmers and theoretical researchers can use to make sure that their results are indeed proved correct.

EVENT PHOTOS:
At CISTER's Facebook page

CISTER's main roles: