Contractor.NET

A .NET validation and specification strengthening tool

From a piece of software to a finite representation

Contractor.NET is an automated tool that takes a piece of software and generates a finite abstract representation of it. By analysing the resulting finite machine, the user can discover potential anomalies in the input contract such as invariants, preconditions or postconditions that are too weak, therefore allowing unwanted behaviour.

Verification of client code

It allows the user to augment the original contract specification for the input class with the inferred typestate information, therefore enabling the verification of client code.

The theory behind Contractor.NET

  • Guido de Caso, Víctor A. Braberman, Diego Garbervetsky, Sebastián Uchitel, Enabledness-based program abstractions for behavior validation. ACM Trans. Softw. Eng. Methodol. 22(3): 25 (2013) [PDF] [BIB]
  • Guido de Caso, Víctor A. Braberman, Diego Garbervetsky, Sebastián Uchitel, Automated Abstractions for Contract Validation. IEEE Trans. Software Eng. 38(1): 141-162 (2012) [PDF] [BIB]
  • Guido de Caso, Víctor Braberman, Diego Garbervetsky, Sebastián Uchitel, Program Abstractions for Behaviour Validation, International Conference on Software Engineering 2011. Honolulu, HI, U.S.A., May 21-28th, 2011 [PDF] [Slides] [Video] [BIB]
  • Guido de Caso, Víctor Braberman, Diego Garbervetsky, Sebastián Uchitel, Automated Abstractions for Contract Validation, IEEE Transactions on Software Engineering (in press) [PDF] [BIB]
  • Guido de Caso, Víctor Braberman, Diego Garbervetsky, Sebastián Uchitel, Contractor for Code Validation, Technical Report, Departamento de Computación, FCEyN, UBA. 2010. [PDF and BIB]
  • Guido de Caso, Behavioural Validation of Software Engineering Artefacts, International Conference on Software Engineering 2010: Doctoral Symposium. Cape Town, South Africa, May 4th, 2010 [PDF] [BIB]
  • Guido de Caso, Víctor Braberman, Diego Garbervetsky, Sebastián Uchitel, Validation of Contracts using Enabledness Preserving Finite State Abstractions, International Conference on Software Engineering 2009. Vancouver, Canada, May 16-24th, 2009 [PDF] [Slides] [Video] [BIB]
  • Edgardo Zoppi, Víctor Braberman, Guido de Caso, Diego Garbervetsky, Sebastián Uchitel, Contractor.NET: inferring typestate properties to enrich code contracts, 1st Workshop on Developing Tools as Plug-ins on TOPI 2011. [PDF]

Tutorial

Tutorial

Meet out awesome team



Sebastian Uchitel, Ph.D.


Victor Braberman, Ph.D.


Diego Garbervetsky, Ph.D.


Edgardo Zoppi, M.Sc.


Leandro Lera Romero, M.Sc.


Fernán Martinelli, M.Sc.