Blocking and Other Enhancements for Bottom-Up Model Generation Methods
Model generation is a problem complementary to theorem proving and is important for fault analysis and debugging of formal specifications of security protocols, programs and terminological definitions, for example. This paper discusses several ways of enhancing the paradigm of bottom-up model generation, with the two main contributions being a new range-restriction transformation and generalized blocking techniques. The range-restriction transformation refines existing transformations to...[Show more]
|Collections||ANU Research Publications|
|Source:||Journal of Automated Reasoning|
|Access Rights:||Open Access|
|01 Portal P and Veraar M Stochastic maximal regularity 2019.pdf||3.35 MB||Adobe PDF|
Items in Open Research are protected by copyright, with all rights reserved, unless otherwise indicated.