🚀 go-pugleaf

Dear Francois,

In 1985 an Esprit project, called ATES, had started. It's objective was the
integration of some advanced techniques in information technologie. Two of 
these were "complete abstraction of data-types and operators" and "formal specification and proof". The partners in the project were CISI Ingenerie (France), Philips Research lab. Brussels, University of Liege (Belgium), University of Twente (The Netherlands), Universite de Paris VI, Commissariat a l'Energie Atomique (France). The project has resulted in a software development system which supports an abstract way of programming and formal specification and proof. The results are collected in a book, see b




elow.

I was one of the ATES-team in Twente and I have been working on formal specification and proof of a finite element library. As a preliminary study we have also formally specified and proven a 1D heat transfer problem. All is contained in my thesis, which reference I give below. At the moment I am working
on a paper entitled something like "Abstraction in, and Specification and Proof of software for a 1D Heat-transfer problem". The precise contents of the paper are not fixed yet.

Eric ten Cate
TWI/TA
Delft University of Technology
Mekelweg 4
2628 CD DELFT
Netherlands
email: tencate@pa.twi.tudelft.nl or tencate@ph.tn.tudelft.nl
phone: (09-31)15-787228

@phdthesis{Cate91a,
   author = "Cate, H. H. ten",
   address = "Enschede",
   month = "september",
   school = "University of Twente",
   title = "Towards Formal Specification and Proof of
	Finite Element Software within the ATES
	Development system",
   year = "1991",
   keywords = "numerical mathematics
   	software engineering"
}

@book{ates-book,
   author = "D. Brocard and H.H. ten Cate and P. Gribomont and A. Puccetti and J. Raguideau and 
A. Remouchamps",
   institution = "Cisi Ing\'{e}nierie",
   title = " Advanced Techniques Integration into Efficient Scientific
Software", 
   type = "ESPRIT Project 1222 (1158), Final Report",
   year = "1991"
}