Browsing by Author "Palasí Lallana, Vicent Ramon"

A Cosemidecision procedure for behavioral equivalence
Palasí Lallana, Vicent Ramon (199601)
External research report
Open AccessWe shall demonstrate that proving the behavioral equivalence of two algebraic specifications is equivalent to proving a set of theorems in a given initial algebra. Thus, it is possible to prove automatically this behavioral ... 
Automatic deduction of the behavioral equivalence between two algebraic specifications
Palasí Lallana, Vicent Ramon (19950101)
External research report
Open AccessWe shall demonstrate that proving the behavioral equivalence of two algebraic specifications is equivalent to proving a set of theorems in a given initial algebra. Thus, it is possible to prove automatically this behavioral ... 
Automatic verification of programs: algorithm ALICE
Palasí Lallana, Vicent Ramon (199606)
External research report
Open AccessThis paper aims to introduce a method for verification of programs, which is fully automatic. This method consists in an algorithm called ALICE which, given a program and an algebraic specification, answers if the ... 
Equivalence between executable OOZE and algebraic specification
Palasí Lallana, Vicent Ramon (199410)
External research report
Open AccessIn this paper two algorithms are presented: one which turns an executable OOZE specification into an algebraic specification and another which does the reverse operation. In this way, we shall be able to prove in a ... 
Reducció de l'equivalència inicial visible a teoremes inductius
Palasí Lallana, Vicent Ramon (199606)
External research report
Open AccessWe prove that checking of the initial visible equivalence between two visible algebraic specification can be reduced to the proof of several inductive theorems on a given initial algebra. 
Reduction of behavioral equivalence to inductive theorems
Palasí Lallana, Vicent Ramon (199601)
External research report
Open AccessWe shall demonstrate that proving the behavioral equivalence of two algebraic specifications can be reduced to proving a set of inductive theorems. So we can prove automatically this behavioral equivalence by applying ... 
Semàntica algebraica del llenguatge AL: l'algorisme alfa
Palasí Lallana, Vicent Ramon (199606)
External research report
Open AccessWe present the AL language. We provide an informal description and give its syntax and semantics in algebraic notation. 
Semàntica externa: una variant interessant de la semàntica de comportament
Palasí Lallana, Vicent Ramon (199606)
External research report
Open AccessStarting from behavioural semantics, a new semantics called "external semantics" is proposed. The aim of this new semantics is to solve the problem of software correctness with respect to an algebraic specification. 
Visible semantics: an algebraic semantics for automatic verification of algorithms
Palasí Lallana, Vicent Ramon (199604)
External research report
Open AccessA new semantics for algebraic specifications, called visible semantics, is defined. Its most notable property is that it is specially suitable for dealing with the problem of program correctness. Some properties of this ...