Go home now Header Background Image
Search
Submission Procedure
share: |
 
Follow us
 
 
 
 
Articles by Topics
Topic F. - Theory of Computation
Topic F.3 - LOGICS AND MEANINGS OF PROGRAMS
Topic F.3.1 - Specifying and Verifying and Reasoning about Programs

J.-R. Abrial:
Formal Methods: Theory Becoming Practice
/jucs_13_5/formal_methods_theory_becoming
page 619 - 628
Vol.13 / Issue 5
M. Alférez, R.E. Lopez-Herrejón, A. Moreira, V. Amaral, A. Egyed:
Consistency Checking in Early Software Product Line Specifications - The VCC Approach
/jucs_20_5/consistency_checking_in_early
page 640 - 665
Vol.20 / Issue 5
A. Armando, S. Ranise:
A Practical Extension Mechanism for Decision Procedures: the Case Study of Universal Presburger Arithmetic
/jucs_7_2/a_practical_extension_mechanism
page 124 - 140
Vol.7 / Issue 2
T. Balanescu, A. J. Cowling, H. Georgescu, M. Gheorghe, M. Holcombe, C. Vertan:
Communicating Stream X-Machines Systems are no more than X-Machines
/jucs_5_9/communicating_stream_x_machines
page 494 - 507
Vol.5 / Issue 9
R. Banach:
Formal Methods
Guest Editorial
/jucs_13_5/formal_methods
page 593 - 601
Vol.13 / Issue 5
K. Baukus, Y. Lakhnech, K. Stahl:
Verification of Parameterized Protocols
/jucs_7_2/verification_of_parameterized_protocols
page 141 - 158
Vol.7 / Issue 2
G. Bella:
What is Correctness of Security Protocols?
/jucs_14_12/what_is_correctness_of
page 2083 - 2107
Vol.14 / Issue 12
U. Berger:
Realisability for Induction and Coinduction with Applications to Constructive Analysis
/jucs_16_18/realisability_for_induction_and
page 2535 - 2555
Vol.16 / Issue 18
N. Berregeb:
Proving Properties for Behavioural Specifications with Term Observation
/jucs_12_10/proving_properties_for_behavioural
page 1413 - 1425
Vol.12 / Issue 10
M. Beynon, J. Rungrattanaubol, J. Sinclair:
Formal Specification from an Observation-Oriented Perspective
/jucs_6_4/formal_specification_from_an
page 407 - 421
Vol.6 / Issue 4
M. Bravetti, A. Casalboni, M. Núñez, I. Rodriguez:
From Theoretical e-Barter Models to Two Alternative Implementations Based on Web Sevices
/jucs_13_13/from_theoretical_ebarter_models
page 2035 - 2075
Vol.13 / Issue 13
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
J. Burton:
Relaxing Atomicity and Verifying Correctness: Considering the Case of an Asynchronous Communication Mechanism
/jucs_11_5/relaxing_atomicity_and_verifying
page 771 - 802
Vol.11 / Issue 5
J. Burton, C. B. Jones:
Investigating Atomicity and Observability
/jucs_11_5/investigating_atomicity_and_observability
page 661 - 686
Vol.11 / Issue 5
E. Börger:
The Origins and the Development of the ASM Method for High Level System Design and Analysis
/jucs_8_1/the_origins_and_the
page 2 - 74
Vol.8 / Issue 1
E. Börger, K.-D. Schewe:
Communication in Abstract State Machines
/jucs_23_2/communication_in_abstract_state
page 129 - 145
Vol.23 / Issue 2
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
F. Chalub, C. Braga:
A Modular Rewriting Semantics for CML
/jucs_10_7/a_modular_rewriting_semantics
page 789 - 807
Vol.10 / Issue 7
G. Ciobanu, M. Rotaru:
A Pi-Calculus Machine
/jucs_6_1/a_pi_calculus_machine
page 39 - 59
Vol.6 / Issue 1
E.M. Clarke, F. Lerda:
Model Checking: Software and Beyond
/jucs_13_5/model_checking_software_and
page 639 - 649
Vol.13 / Issue 5
M. Clavel, M. Palomino, A. Riesco:
Introducing the ITP Tool: a Tutorial
/jucs_12_11/introducing_the_itp_tool
page 1618 - 1650
Vol.12 / Issue 11
J.M. Cleva, I. Pita:
Verification of CRWL Programs with Rewriting Logic
/jucs_12_11/verification_of_crwl_programs
page 1594 - 1617
Vol.12 / Issue 11
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
M. Denford, A. Solomon, J. Leaney, T. O'Neill:
Architectural Abstraction as Transformation of Poset Labelled Graphs
/jucs_10_10/architectural_abstraction_as_transformation
page 1408 - 1428
Vol.10 / Issue 10
C. Domínguez, J. Rubio, F. Sergeraert:
Modeling Inheritance as Coercion in the Kenzo System
/jucs_12_12/modeling_inheritance_as_coercion
page 1701 - 1730
Vol.12 / Issue 12
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
H.-D. Ehrich, M. Kollmann, R. Pinger:
Checking Object System Designs Incrementally
/jucs_9_2/checking_object_system_designs
page 106 - 119
Vol.9 / Issue 2
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
A. Gargantini, E. Riccobene, P. Scandurra:
A Metamodel-based Language and a Simulation Engine for Abstract State Machines
/jucs_14_12/a_metamodel_based_language
page 1949 - 1983
Vol.14 / Issue 12
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
L. Groves:
Reasoning about Nonblocking Concurrency
/jucs_15_1/reasoning_about_nonblocking_concurrency
page 72 - 111
Vol.15 / Issue 1
W. Guttmann, H. Partsch, W. Schulte, T. Vullinghs:
Tool Support for the Interactive Derivation of Formally Correct Functional Programs
/jucs_9_2/tool_support_for_the
page 173 - 188
Vol.9 / Issue 2
F. C. Gärtner:
Transformational Approaches to the Specification and Verification of Fault-Tolerant Systems: Formal Background and Classification
/jucs_5_10/transformational_approaches_to_the
page 668 - 692
Vol.5 / Issue 10
A. Hall:
Realising the Benefits of Formal Methods
/jucs_13_5/realising_the_benefits_of
page 669 - 678
Vol.13 / Issue 5
J. Harrison:
Floating-Point Verification
/jucs_13_5/floating_point_verification
page 629 - 638
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
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
M. Kronenburg, C. Peper:
Application of the FOREST Approach to the Light Control Case Study
/jucs_6_7/application_of_the_forest
page 679 - 703
Vol.6 / Issue 7
A. Lamei, M.S. Fallah:
Rewriting-Based Enforcement of Noninterference in Programs with Observable Intermediate Values
/jucs_22_7/rewriting_based_enforcement_of
page 956 - 991
Vol.22 / Issue 7
A. MacDonald, D. Carrington:
Some Elements of Z Specification Style: Structuring Techniques
/jucs_6_12/some_elements_of_z
page 1203 - 1225
Vol.6 / Issue 12
S. Maharaj, C. Shankland:
A Survey of Formal Methods Applied to Leader Election in IEEE 1394
/jucs_6_11/a_survey_of_formal
page 1145 - 1163
Vol.6 / Issue 11
M.A. Martins:
Behavioral Institutions and Refinements in Generalized Hidden Logics
/jucs_12_8/behavioral_institutions_and_refinements
page 1020 - 1049
Vol.12 / Issue 8
H.-S. Min, S.-M. Chung, J.-Y. Choi:
Deriving System Behavior from UML State Machine Diagram: Applied to Missile Project
/jucs_19_1/deriving_system_behavior_from
page 53 - 77
Vol.19 / Issue 1
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
K. Ogata, K. Futatsugi:
Compositionally Writing Proof Scores of Invariants in the OTS/CafeOBJ Method
/jucs_19_6/compositionally_writing_proof_scores
page 771 - 804
Vol.19 / Issue 6
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
J. N. Oliveira:
"Bagatelle in C arranged for VDM SoLo"
/jucs_7_8/bagatelle_in_c_arranged
page 754 - 781
Vol.7 / Issue 8
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
P.R. Ribeiro, M.A. Barbosa, L.S. Barbosa:
Generic Process Algebra: A Programming Challenge
/jucs_12_7/generic_process_algebra_a
page 922 - 937
Vol.12 / Issue 7
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. Ruf:
RAVEN: Real-Time Analyzing and Verification Environment
/jucs_7_1/raven_real_time_analyzing
page 89 - 104
Vol.7 / Issue 1
J. Rushby:
Automated Formal Methods Enter the Mainstream
/jucs_13_5/automated_formal_methods_enter
page 650 - 660
Vol.13 / Issue 5
G. Schellhorn:
Verification of ASM Refinements Using Generalized Forward Simulation
/jucs_7_11/verification_of_asm_refinements
page 952 - 979
Vol.7 / Issue 11
G. Schellhorn:
ASM Refinement Preserving Invariants
/jucs_14_12/asm_refinement_preserving_invariants
page 1929 - 1948
Vol.14 / Issue 12
C. Cerschi Seceleanu, T. Seceleanu:
Synchronization Can Improve Reactive Systems Control and Modularity
/jucs_10_10/synchronization_can_improve_reactive
page 1429 - 1468
Vol.10 / Issue 10
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
L. J. Steggles:
Specifying and Verifying Real-Time Systems using Second-Order Algebraic Methods: A Case Study of the Railroad Crossing Controller
/jucs_6_4/specifying_and_verifying_real
page 460 - 473
Vol.6 / Issue 4
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
M. Viroli, A. Omicini:
Modelling Agents as Observable Sources
/jucs_8_4/modelling_agents_as_observable
page 423 - 451
Vol.8 / Issue 4
J. Woodcock, R. Banach:
The Verification Grand Challenge
/jucs_13_5/the_verification_grand_challenge
page 661 - 668
Vol.13 / Issue 5
B. Zouari:
A Structure Causality Relation for Liveness Characterisation in Petri Nets
/jucs_12_2/a_structure_causality_relation
page 214 - 232
Vol.12 / Issue 2
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