| Variability-based model transformation: formal foundation and application |
4 |
| A formal approach for detection of security flaws in the android permission system |
2 |
| A UTP approach for rTiMo |
2 |
| Toward automatic verification of quantum programs |
2 |
| Multiple model synchronization with multiary delta lenses with amendment and K-Putput |
2 |
| Alternative shaper: a model for automatic design generation |
2 |
| Finding suitable variability abstractions for lifted analysis |
2 |
| A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency |
1 |
| Battery-aware scheduling in low orbit: the GomX-3 case |
1 |
| ProFeat: feature-oriented engineering for family-based probabilistic model checking |
1 |
| Model-based testing of probabilistic systems |
1 |
| A UTP semantics for communicating processes with shared variables and its formal encoding in PVS |
1 |
| Bisimulation and Coinduction Enhancements: A Historical Perspective |
1 |
| Automated circular assume-guarantee reasoning |
1 |
| Model-based problem solving for university timetable validation and improvement |
1 |
| An explicit transition system construction approach to LTL satisfiability checking |
1 |
| Formally sound implementations of security protocols with JavaSPI |
1 |
| Formal analysis of the kinematic Jacobian in screw theory |
1 |
| Automating Event-B invariant proofs by rippling and proof patching |
1 |
| Consistency-preserving refactoring of refinement structures in Event-B models |
1 |
| Milestones from the Pure Lisp theorem prover to ACL2 |
1 |
| Fifty years of Hoare's logic |
1 |
| Tests and proofs for custom data generators |
0 |
| How testing helps to diagnose proof failures |
0 |
| Assembling a prehistory for formal methods: a personal view |
0 |
| From LCF to Isabelle/HOL |
0 |
| Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving |
0 |
| A modeling and verification framework for optical quantum circuits |
0 |
| Investigating the limits of rely/guarantee relations based on a concurrent garbage collector example |
0 |
| Formal reliability analysis of redundancy architectures |
0 |
| Extensional Petri net |
0 |
| GPU-accelerated steady-state computation of large probabilistic Boolean networks |
0 |
| Code obfuscation against abstraction refinement attacks |
0 |
| Adaptive distinguishing test cases of nondeterministic finite state machines: test case derivation and length estimation |
0 |
| Formal verification and quantitative metrics of MPSoC data dynamics |
0 |
| The symbiosis of concurrency and verification: teaching and case studies |
0 |
| Mechanized proofs of opacity: a comparison of two techniques |
0 |
| A fully verified container library |
0 |
| Hybrid statistical estimation of mutual information and its application to information flow |
0 |
| Automated mutual induction proof in separation logic |
0 |
| Estimating costs of multi-component enterprise applications |
0 |
| Discovering and correcting a deadlock in a channel implementation |
0 |
| Cut branches before looking for bugs: certifiably sound verification on relaxed slices |
0 |
| A semantics comparison workbench for a concurrent, asynchronous, distributed programming language |
0 |
| A formal verification technique for behavioural model-to-model transformations |
0 |
| Read atomic transactions with prevention of lost updates: ROLA and its formal analysis |
0 |
| Interactive verification of architectural design patterns in FACTum |
0 |
| A verification-driven framework for iterative design of controllers |
0 |
| Unifying separation logic and region logic to allow interoperability |
0 |
| Parameterized verification of monotone information systems |
0 |
