J.-R. Abrial:
Formal Methods: Theory Becoming Practice
/jucs_13_5/formal_methods_theory_becoming

page 619 - 628
Vol.13 / Issue 5

M. Alpuente, M. del Mar Gallardo, E. Pimentel, A. Villanueva:
Verifying Real-Time Properties of tccp Programs
/jucs_12_11/verifying_real_time_properties

page 1551 - 1573
Vol.12 / Issue 11

D. B. Aredo:
A Framework for Semantics of UML Sequence Diagrams in PVS
/jucs_8_7/a_framework_for_semantics

page 674 - 697
Vol.8 / Issue 7

R. Banach:
Formal Methods
Guest Editorial
/jucs_13_5/formal_methods

page 593 - 601
Vol.13 / Issue 5

R. Berghammer, T. Hoffmann:
Modeling Sequences within the RelView System
/jucs_7_2/modeling_sequences_within_the

page 107 - 123
Vol.7 / Issue 2

A.D. Brucker, F. Rittinger, B. Wolff:
HOL-Z 2.0: A Proof Environment for Z-Specifications
/jucs_9_2/hol_z_2

page 152 - 172
Vol.9 / Issue 2

E. Börger, L. Mearelli:
Integrating ASMs into the Software Development Life Cycle
/jucs_3_5/integrating_asm

page 603 - 665
Vol.3 / Issue 5

D. Cansell, D. Mery, S. Merz:
Diagram Refinements for the Design of Reactive Systems
/jucs_7_2/diagram_refinements_for_the

page 159 - 174
Vol.7 / Issue 2

E.M. Clarke, F. Lerda:
Model Checking: Software and Beyond
/jucs_13_5/model_checking_software_and

page 639 - 649
Vol.13 / Issue 5

J. Crossley, I. Poernomo:
Fred: An Approach to Generating Real, Correct, Reusable Programs from Proofs
/jucs_7_1/fred_an_approach_to

page 71 - 88
Vol.7 / Issue 1

D. Drusinsky:
On-line Monitoring of Metric Temporal Logic with Time-Series Constraints Using Alternating Finite Automata
/jucs_12_5/on_line_monitoring_of

page 482 - 498
Vol.12 / Issue 5

D. Drusinsky, M.-T. Shing:
Monitoring Temporal Logic Specifications Combined with Time Series Constraints
/jucs_9_11/monitoring_temporal_logic_specification

page 1261 - 1276
Vol.9 / Issue 11

W. Fokkink, J. Pang:
Variations on Itai-Rodeh Leader Election for Anonymous Rings and their Analysis in PRISM
/jucs_12_8/variations_on_itai_rodeh

page 981 - 1006
Vol.12 / Issue 8

L. Fuentes, D. Jiménez, M. Pinto:
Development of Ambient Intelligence Applications using Components and Aspects
/jucs_12_3/development_of_ambient_intelligence

page 236 - 251
Vol.12 / Issue 3

S. Glesner:
Using Program Checking to Ensure the Correctness of Compiler Implementations
/jucs_9_3/using_program_checking_to

page 191 - 222
Vol.9 / Issue 3

A. Hall:
Realising the Benefits of Formal Methods
/jucs_13_5/realising_the_benefits_of

page 669 - 678
Vol.13 / Issue 5

C.L. Heitmeyer:
Formal Methods for Specifying, Validating, and Verifying Requirements
/jucs_13_5/formal_methods_for_specifying

page 607 - 618
Vol.13 / Issue 5

H. Hojjat, H. Nakhost, M. Sirjani:
Integrating Module Checking and Deduction in a Formal Proof for the Perlman Spanning Tree Protocol (STP)
/jucs_13_13/integrating_module_checking_and

page 2076 - 2104
Vol.13 / Issue 13

M. J. Hornos:
FBT: A Tool for Applying Interval Logic Specifications to On-the-fly Model Checking
/jucs_10_11/fbt_a_tool_for

page 1498 - 1518
Vol.10 / Issue 11

C. B. Jones:
The Transition from VDL to VDM
/jucs_7_8/the_transition_from_VDL

page 631 - 640
Vol.7 / Issue 8

T. A. Junttila:
Computational Complexity of the Place/Transition-Net Symmetry Reduction Method
/jucs_7_4/computational_complexity_of_the

page 307 - 326
Vol.7 / Issue 4

R. Malik, R. Mühlfeld:
A Case Study in Verification of UML Statecharts: the PROFIsafe Protocol
/jucs_9_2/a_case_study_in

page 138 - 151
Vol.9 / Issue 2

L. Mearelli:
Refining an ASM Specification of the Production Cell to C++ Code
/jucs_3_5/production_cell

page 666 - 688
Vol.3 / Issue 5

J. Mullins:
Nondeterministic Admissible Interference
/jucs_6_11/nondeterministic_admissible_interference

page 1054 - 1070
Vol.6 / Issue 11

D. Méry, S. Merz:
Specification and Refinement of Access Control
/jucs_13_8/specification_and_refinement_of

page 1073 - 1093
Vol.13 / Issue 8

T.V.N. Nguyen, F. Irigoin:
Alias Verification for Fortran Code Optimization
/jucs_9_3/alias_verification_for_fortran

page 270 - 297
Vol.9 / Issue 3

E.-R. Olderog, H. Dierks:
Moby/RT: A Tool for Specification and Verification of Real-Time Systems
/jucs_9_2/mobyrt_a_tool_for

page 88 - 105
Vol.9 / Issue 2

S.K. Rajamani:
Software Is More Than Code
/jucs_13_5/software_is_more_than

page 602 - 606
Vol.13 / Issue 5

W. Reif, G. Schellhorn, T. Vollmer, J. Ruf:
Correctness of Efficient Real-Time Model Checking
/jucs_7_2/correctness_of_efficient_real

page 194 - 209
Vol.7 / Issue 2

J. Rothe, H. Tews, B. Jacobs:
The Coalgebraic Class Specification Language CCSL
/jucs_7_2/the_coalgebraic_class_specification

page 175 - 193
Vol.7 / Issue 2

J. Rushby:
Automated Formal Methods Enter the Mainstream
/jucs_13_5/automated_formal_methods_enter

page 650 - 660
Vol.13 / Issue 5

S. Sasaki, T. Nishihara, D. Ando, M. Fujita:
Hardware/Software Co-design and Verification Methodology from System Level Based on System Dependence Graph
/jucs_13_13/hardware_software_codesign_and

page 1972 - 2001
Vol.13 / Issue 13

G. Schellhorn:
Verification of ASM Refinements Using Generalized Forward Simulation
/jucs_7_11/verification_of_asm_refinements

page 952 - 979
Vol.7 / Issue 11

M. Sirjani, F.S. de Boer, A. Movaghar:
Modular Verification of a Component-Based Actor Language
/jucs_11_10/modular_verificatin_of_a

page 1695 - 1717
Vol.11 / Issue 10

M. Sirjani, A. Movaghar, A. Shali, F. S. de Boer:
Model Checking, Automated Abstraction, and Compositional Verification of Rebeca Models
/jucs_11_6/model_checking_automated_abstraction

page 1054 - 1082
Vol.11 / Issue 6

G. Smith, C. Fidge:
Incremental Development of Real-Time Requirements: The Light Control Case Study
/jucs_6_7/incremental_development_of_real

page 704 - 730
Vol.6 / Issue 7

K. Strötmann:
The Constrained Shortest Path Problem: A Case Study in Using ASMs
/jucs_3_4/shortest_path_problem

page 304 - 319
Vol.3 / Issue 4

R. F. Stärk, S. Nanchen:
A Logic for Abstract State Machines
/jucs_7_11/a_logic_for_abstract

page 980 - 1005
Vol.7 / Issue 11

I. Traoré:
An Outline of PVS Semantics for UML Statecharts
/jucs_6_11/an_outline_of_pvs

page 1088 - 1108
Vol.6 / Issue 11

H. Treseler, O. Stursberg, P. W. H. Chung, S. Yang:
An Open Software Architecture for the Verification of Industrial Controllers
/jucs_7_1/an_open_software_architecture

page 37 - 53
Vol.7 / Issue 1

J. Woodcock, R. Banach:
The Verification Grand Challenge
/jucs_13_5/the_verification_grand_challenge

page 661 - 668
Vol.13 / Issue 5

W. Zimmermann, T. Gaul:
On the Construction of Correct Compiler Back-Ends: An ASM-Approach
/jucs_3_5/correct_compiler

page 504 - 567
Vol.3 / Issue 5

L. Zuck, A. Pnueli, Y. Fang, B. Goldberg:
VOC: A Methodology for the Translation Validation of OptimizingCompilers
/jucs_9_3/voc_a_methodology_for

page 223 - 247
Vol.9 / Issue 3

F. de Oliveira Jr., R. Lima, M. Cornelio, S. Soares, P. Maciel, R. Barreto, M. Oliveira Jr., E. Tavares:
CML: C Modeling Language
/jucs_13_6/cml_c_modeling_language

page 682 - 700
Vol.13 / Issue 6

J.A. Andrew van der Poll, P. Kotzé, W. Adrian Labuschagne:
Automated Support for Enterprise Information Systems
/jucs_10_11/automated_support_for_enterprise

page 1519 - 1539
Vol.10 / Issue 11