4 papers
An Adequacy Theorem Between Mixed Powerdomains and Probabilistic Concurrency
Renato Neves
We present an adequacy theorem for a concurrent extension of probabilistic GCL. The underlying denotational semantics is based on the so-called mixed powerdomains, which combine no…
An adequacy theorem between mixed powerdomains and probabilistic concurrency (extended version)
Renato Neves
We present an adequacy theorem for a concurrent extension of probabilistic GCL. The underlying denotational semantics is based on the so-called mixed powerdomains, which combine no…
An Adequate While-Language for Stochastic Hybrid Computation
Renato Neves, José Proença, Juliana Souza
We introduce a language for formally reasoning about programs that combine differential constructs with probabilistic ones. The language harbours, for example, such systems as adap…
Formal Simulation and Visualisation of Hybrid Programs
Pedro Mendes, Ricardo Correia, Renato Neves +1
The design and analysis of systems that combine computational behaviour with physical processes' continuous dynamics - such as movement, velocity, and voltage - is a famous, challe…