Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

16

AFP
2015
Springer

favoriteEmaildiscussreport

20views Formal Methods» more AFP 2015»

Generating Cases from Labeled Subgoals

8 years 6 days ago

Generating Cases from Labeled Subgoals

Download afp.sourceforge.net

Isabelle/Isar provides named cases to structure proofs. This article contains an implementation of a proof method casify, which can be used to easily extend proof tools with support for named cases. Such a proof tool must produce labeled subgoals, which are then interpreted by casify. As examples, this work contains veriﬁcation condition generators producing named cases for three languages: The Hoare language from HOL/Library, a monadic language for computations with failure (inspired by the AutoCorres tool), and a language of conditional expressions. These VCGs are demonstrated by a number of example programs. 1

Lars Noschinski

Real-time Traffic

AFP 2015 | Formal Methods |

claim paper

Related Content

» Learning Similar Tasks From Observation and Practice

» Generating labels from clicks

» Generative and Discriminative Learning with Unknown Labeling Bias

» Generating Transition Probabilities for Automatic ModelBased Test Generation

» Tabu Search Heuristic for PointFeature Cartographic Label Placement

» BP2 Beyond pairwise Belief Propagation labeling by approximating Kikuchi free energies

» Semantic Labeling Of Track Events Using Time Series Segmentation And Shape Analysis

» An Extension of Wilkinsons Algorithm for Positioning Tick Labels on Axes

» Approximate Labeling via Graph Cuts Based on Linear Programming

» Analysing the behaviour of distributed software architectures a case study

Post Info
More Details (n/a)

Added	13 Apr 2016
Updated	13 Apr 2016
Type	Journal
Year	2015
Where	AFP
Authors	Lars Noschinski

Comments (0)