Subjects -> COMPUTER SCIENCE (Total: 2313 journals)
    - ANIMATION AND SIMULATION (33 journals)
    - ARTIFICIAL INTELLIGENCE (133 journals)
    - AUTOMATION AND ROBOTICS (116 journals)
    - CLOUD COMPUTING AND NETWORKS (75 journals)
    - COMPUTER ARCHITECTURE (11 journals)
    - COMPUTER ENGINEERING (12 journals)
    - COMPUTER GAMES (23 journals)
    - COMPUTER PROGRAMMING (25 journals)
    - COMPUTER SCIENCE (1305 journals)
    - COMPUTER SECURITY (59 journals)
    - DATA BASE MANAGEMENT (21 journals)
    - DATA MINING (50 journals)
    - E-BUSINESS (21 journals)
    - E-LEARNING (30 journals)
    - ELECTRONIC DATA PROCESSING (23 journals)
    - IMAGE AND VIDEO PROCESSING (42 journals)
    - INFORMATION SYSTEMS (109 journals)
    - INTERNET (111 journals)
    - SOCIAL WEB (61 journals)
    - SOFTWARE (43 journals)
    - THEORY OF COMPUTING (10 journals)

COMPUTER SCIENCE (1305 journals)            First | 1 2 3 4 5 6 7 | Last

Showing 201 - 400 of 872 Journals sorted alphabetically
Computational Communication Research     Open Access   (Followers: 2)
Computational Complexity     Hybrid Journal   (Followers: 5)
Computational Condensed Matter     Open Access   (Followers: 1)
Computational Ecology and Software     Open Access   (Followers: 9)
Computational Economics     Hybrid Journal   (Followers: 13)
Computational Geosciences     Hybrid Journal   (Followers: 16)
Computational Linguistics     Open Access   (Followers: 27)
Computational Management Science     Hybrid Journal  
Computational Mathematics and Modeling     Hybrid Journal   (Followers: 8)
Computational Mechanics     Hybrid Journal   (Followers: 13)
Computational Methods and Function Theory     Hybrid Journal  
Computational Molecular Bioscience     Open Access   (Followers: 1)
Computational Optimization and Applications     Hybrid Journal   (Followers: 10)
Computational Particle Mechanics     Hybrid Journal   (Followers: 1)
Computational Science and Discovery     Full-text available via subscription   (Followers: 3)
Computational Science and Techniques     Open Access  
Computational Statistics     Hybrid Journal   (Followers: 16)
Computational Statistics & Data Analysis     Hybrid Journal   (Followers: 37)
Computational Toxicology     Hybrid Journal  
Computer     Full-text available via subscription   (Followers: 178)
Computer Aided Surgery     Open Access   (Followers: 5)
Computer Applications in Engineering Education     Hybrid Journal   (Followers: 6)
Computer Communications     Hybrid Journal   (Followers: 18)
Computer Engineering and Applications Journal     Open Access   (Followers: 8)
Computer Journal     Hybrid Journal   (Followers: 7)
Computer Methods in Applied Mechanics and Engineering     Hybrid Journal   (Followers: 29)
Computer Methods in Biomechanics and Biomedical Engineering     Hybrid Journal   (Followers: 12)
Computer Methods in Biomechanics and Biomedical Engineering : Imaging & Visualization     Hybrid Journal  
Computer Music Journal     Hybrid Journal   (Followers: 22)
Computer Physics Communications     Hybrid Journal   (Followers: 11)
Computer Science - Research and Development     Hybrid Journal   (Followers: 9)
Computer Science and Engineering     Open Access   (Followers: 14)
Computer Science and Information Technology     Open Access   (Followers: 11)
Computer Science Education     Hybrid Journal   (Followers: 18)
Computer Science Journal     Open Access   (Followers: 22)
Computer Science Review     Hybrid Journal   (Followers: 12)
Computer Standards & Interfaces     Hybrid Journal   (Followers: 3)
Computer Supported Cooperative Work (CSCW)     Hybrid Journal   (Followers: 10)
Computer-aided Civil and Infrastructure Engineering     Hybrid Journal   (Followers: 9)
Computer-Aided Design and Applications     Hybrid Journal   (Followers: 6)
Computers     Open Access   (Followers: 1)
Computers & Chemical Engineering     Hybrid Journal   (Followers: 11)
Computers & Education     Hybrid Journal   (Followers: 94)
Computers & Electrical Engineering     Hybrid Journal   (Followers: 11)
Computers & Geosciences     Hybrid Journal   (Followers: 30)
Computers & Mathematics with Applications     Full-text available via subscription   (Followers: 11)
Computers & Structures     Hybrid Journal   (Followers: 46)
Computers & Education Open     Open Access   (Followers: 4)
Computers & Industrial Engineering     Hybrid Journal   (Followers: 7)
Computers and Composition     Hybrid Journal   (Followers: 13)
Computers and Education: Artificial Intelligence     Open Access   (Followers: 7)
Computers and Electronics in Agriculture     Hybrid Journal   (Followers: 11)
Computers and Geotechnics     Hybrid Journal   (Followers: 13)
Computers in Biology and Medicine     Hybrid Journal   (Followers: 8)
Computers in Entertainment     Hybrid Journal   (Followers: 3)
Computers in Human Behavior Reports     Open Access   (Followers: 3)
Computers in Industry     Hybrid Journal   (Followers: 7)
Computers in the Schools     Hybrid Journal   (Followers: 8)
Computers, Environment and Urban Systems     Hybrid Journal   (Followers: 13)
Computerworld Magazine     Free   (Followers: 2)
Computing     Hybrid Journal   (Followers: 2)
Computing and Software for Big Science     Hybrid Journal   (Followers: 1)
Computing and Visualization in Science     Hybrid Journal   (Followers: 4)
Computing in Science & Engineering     Full-text available via subscription   (Followers: 31)
Computing Reviews     Full-text available via subscription   (Followers: 1)
Concurrency and Computation: Practice & Experience     Hybrid Journal   (Followers: 1)
Connection Science     Open Access  
Control Engineering Practice     Hybrid Journal   (Followers: 49)
Cryptologia     Hybrid Journal   (Followers: 3)
CSI Transactions on ICT     Hybrid Journal   (Followers: 2)
Cuadernos de Documentación Multimedia     Open Access  
Current Science     Open Access   (Followers: 147)
Cyber-Physical Systems     Hybrid Journal  
Cyberspace : Jurnal Pendidikan Teknologi Informasi     Open Access  
DAIMI Report Series     Open Access  
Data     Open Access   (Followers: 4)
Data & Policy     Open Access   (Followers: 4)
Data Science     Open Access   (Followers: 5)
Data Science and Engineering     Open Access   (Followers: 3)
Data Technologies and Applications     Hybrid Journal   (Followers: 243)
Data-Centric Engineering     Open Access   (Followers: 2)
Datenbank-Spektrum     Hybrid Journal   (Followers: 1)
Datenschutz und Datensicherheit - DuD     Hybrid Journal  
Decision Analytics     Open Access   (Followers: 3)
Decision Support Systems     Hybrid Journal   (Followers: 14)
Design Journal : An International Journal for All Aspects of Design     Hybrid Journal   (Followers: 38)
Digital Biomarkers     Open Access   (Followers: 1)
Digital Chemical Engineering     Open Access   (Followers: 2)
Digital Chinese Medicine     Open Access  
Digital Creativity     Hybrid Journal   (Followers: 12)
Digital Experiences in Mathematics Education     Hybrid Journal   (Followers: 3)
Digital Finance : Smart Data Analytics, Investment Innovation, and Financial Technology     Hybrid Journal   (Followers: 3)
Digital Geography and Society     Open Access   (Followers: 2)
Digital Government : Research and Practice     Open Access   (Followers: 2)
Digital Health     Open Access   (Followers: 10)
Digital Journalism     Hybrid Journal   (Followers: 8)
Digital Medicine     Open Access   (Followers: 3)
Digital Platform: Information Technologies in Sociocultural Sphere     Open Access   (Followers: 4)
Digital Policy, Regulation and Governance     Hybrid Journal   (Followers: 3)
Digital War     Hybrid Journal   (Followers: 2)
Digitale Welt : Das Wirtschaftsmagazin zur Digitalisierung     Hybrid Journal  
Digitális Bölcsészet / Digital Humanities     Open Access   (Followers: 2)
Disaster Prevention and Management     Hybrid Journal   (Followers: 28)
Discours     Open Access   (Followers: 1)
Discourse & Communication     Hybrid Journal   (Followers: 27)
Discover Internet of Things     Open Access   (Followers: 3)
Discrete and Continuous Models and Applied Computational Science     Open Access  
Discrete Event Dynamic Systems     Hybrid Journal   (Followers: 3)
Discrete Mathematics & Theoretical Computer Science     Open Access   (Followers: 1)
Discrete Optimization     Full-text available via subscription   (Followers: 6)
Displays     Hybrid Journal  
Distributed and Parallel Databases     Hybrid Journal   (Followers: 2)
e-learning and education (eleed)     Open Access   (Followers: 40)
Ecological Indicators     Hybrid Journal   (Followers: 22)
Ecological Informatics     Hybrid Journal   (Followers: 4)
Ecological Management & Restoration     Hybrid Journal   (Followers: 16)
Ecosystems     Hybrid Journal   (Followers: 33)
Edu Komputika Journal     Open Access   (Followers: 1)
Education and Information Technologies     Hybrid Journal   (Followers: 54)
Educational Philosophy and Theory     Hybrid Journal   (Followers: 11)
Educational Psychology in Practice: theory, research and practice in educational psychology     Hybrid Journal   (Followers: 13)
Educational Research and Evaluation: An International Journal on Theory and Practice     Hybrid Journal   (Followers: 8)
Educational Theory     Hybrid Journal   (Followers: 9)
Egyptian Informatics Journal     Open Access   (Followers: 6)
Electronic Commerce Research and Applications     Hybrid Journal   (Followers: 5)
Electronic Design     Partially Free   (Followers: 155)
electronic Journal of Health Informatics     Open Access   (Followers: 7)
Electronic Letters on Computer Vision and Image Analysis     Open Access   (Followers: 10)
Elektron     Open Access  
Empirical Software Engineering     Hybrid Journal   (Followers: 10)
Energy for Sustainable Development     Hybrid Journal   (Followers: 13)
Engineering & Technology     Hybrid Journal   (Followers: 23)
Engineering Applications of Computational Fluid Mechanics     Open Access   (Followers: 23)
Engineering Computations     Hybrid Journal   (Followers: 3)
Engineering Economist, The     Hybrid Journal   (Followers: 4)
Engineering Optimization     Hybrid Journal   (Followers: 11)
Engineering With Computers     Hybrid Journal   (Followers: 5)
Enterprise Information Systems     Hybrid Journal   (Followers: 2)
Entertainment Computing     Hybrid Journal   (Followers: 2)
Environmental and Ecological Statistics     Hybrid Journal   (Followers: 7)
Environmental Communication: A Journal of Nature and Culture     Hybrid Journal   (Followers: 16)
EPJ Data Science     Open Access   (Followers: 11)
ESAIM: Control Optimisation and Calculus of Variations     Open Access   (Followers: 3)
Ethics and Information Technology     Hybrid Journal   (Followers: 66)
eTransportation     Open Access   (Followers: 1)
EURO Journal on Computational Optimization     Open Access   (Followers: 4)
EuroCALL Review     Open Access   (Followers: 1)
European Food Research and Technology     Hybrid Journal   (Followers: 8)
European Journal of Combinatorics     Full-text available via subscription   (Followers: 3)
European Journal of Computational Mechanics     Hybrid Journal   (Followers: 1)
European Journal of Information Systems     Hybrid Journal   (Followers: 97)
European Journal of Law and Technology     Open Access   (Followers: 21)
European Journal of Political Theory     Hybrid Journal   (Followers: 31)
Evolutionary Computation     Hybrid Journal   (Followers: 12)
Fibreculture Journal     Open Access   (Followers: 9)
Finite Fields and Their Applications     Full-text available via subscription   (Followers: 5)
Fixed Point Theory and Applications     Open Access  
Focus on Catalysts     Full-text available via subscription  
Focus on Pigments     Full-text available via subscription   (Followers: 3)
Focus on Powder Coatings     Full-text available via subscription   (Followers: 5)
Forensic Science International: Digital Investigation     Full-text available via subscription   (Followers: 363)
Formal Aspects of Computing     Hybrid Journal   (Followers: 3)
Formal Methods in System Design     Hybrid Journal   (Followers: 7)
Forschung     Hybrid Journal   (Followers: 1)
Foundations and Trends® in Communications and Information Theory     Full-text available via subscription   (Followers: 6)
Foundations and Trends® in Databases     Full-text available via subscription   (Followers: 2)
Foundations and Trends® in Human-Computer Interaction     Full-text available via subscription   (Followers: 5)
Foundations and Trends® in Information Retrieval     Full-text available via subscription   (Followers: 30)
Foundations and Trends® in Networking     Full-text available via subscription   (Followers: 1)
Foundations and Trends® in Signal Processing     Full-text available via subscription   (Followers: 6)
Foundations and Trends® in Theoretical Computer Science     Full-text available via subscription   (Followers: 1)
Foundations of Computational Mathematics     Hybrid Journal   (Followers: 1)
Foundations of Computing and Decision Sciences     Open Access  
Frontiers in Computational Neuroscience     Open Access   (Followers: 24)
Frontiers in Computer Science     Open Access   (Followers: 1)
Frontiers in Digital Health     Open Access   (Followers: 4)
Frontiers in Digital Humanities     Open Access   (Followers: 9)
Frontiers in ICT     Open Access  
Frontiers in Neuromorphic Engineering     Open Access   (Followers: 2)
Frontiers in Research Metrics and Analytics     Open Access   (Followers: 5)
Frontiers of Computer Science in China     Hybrid Journal   (Followers: 2)
Frontiers of Environmental Science & Engineering     Hybrid Journal   (Followers: 3)
Frontiers of Information Technology & Electronic Engineering     Hybrid Journal  
Fuel Cells Bulletin     Full-text available via subscription   (Followers: 10)
Functional Analysis and Its Applications     Hybrid Journal   (Followers: 2)
Future Computing and Informatics Journal     Open Access   (Followers: 1)
Future Generation Computer Systems     Hybrid Journal   (Followers: 2)
Geo-spatial Information Science     Open Access   (Followers: 8)
Geoforum Perspektiv     Open Access   (Followers: 1)
GeoInformatica     Hybrid Journal   (Followers: 7)
Geoinformatics FCE CTU     Open Access   (Followers: 5)
GetMobile : Mobile Computing and Communications     Full-text available via subscription   (Followers: 2)
Government Information Quarterly     Hybrid Journal   (Followers: 29)
Granular Computing     Hybrid Journal  
Graphics and Visual Computing     Open Access  
Grey Room     Hybrid Journal   (Followers: 21)
Group Dynamics : Theory, Research, and Practice     Full-text available via subscription   (Followers: 16)
Groups, Complexity, Cryptology     Open Access   (Followers: 2)
HardwareX     Open Access  
Harvard Data Science Review     Open Access   (Followers: 2)

  First | 1 2 3 4 5 6 7 | Last

Similar Journals
Journal Cover
Formal Methods in System Design
Journal Prestige (SJR): 0.445
Citation Impact (citeScore): 2
Number of Followers: 7  
 
  Hybrid Journal Hybrid journal (It can contain Open Access articles)
ISSN (Print) 1572-8102 - ISSN (Online) 0925-9856
Published by Springer-Verlag Homepage  [2468 journals]
  • Termination of triangular polynomial loops

    • Free pre-print version: Loading...

      Abstract: Abstract We consider the problem of proving termination for triangular weakly non-linear loops (twn-loops) over some ring \(\mathcal {S}\) like \(\mathbb {Z}\) , \(\mathbb {Q}\) , or \(\mathbb {R}\) . The guard of such a loop is an arbitrary quantifier-free Boolean formula over (possibly non-linear) polynomial inequations, and the body is a single assignment of the form \(\begin{bmatrix} x_1\\ \ldots \\ x_d \end{bmatrix} \leftarrow \begin{bmatrix} c_1 \cdot x_1 + p_1\\ \ldots \\ c_d \cdot x_d + p_d \end{bmatrix}\) where each \(x_i\) is a variable, \(c_i \in \mathcal {S}\) , and each \(p_i\) is a (possibly non-linear) polynomial over \(\mathcal {S}\) and the variables \(x_{i+1},\ldots ,x_{d}\) . We show that the question of termination can be reduced to the existential fragment of the first-order theory of \(\mathcal {S}\) . For loops over \(\mathbb {R}\) , our reduction implies decidability of termination. For loops over \(\mathbb {Z}\) and \(\mathbb {Q}\) , it proves semi-decidability of non-termination. Furthermore, we present a transformation to convert certain non-twn-loops into twn-form. Then the original loop terminates iff the transformed loop terminates over a specific subset of \(\mathbb {R}\) , which can also be checked via our reduction. Moreover, we formalize a technique to linearize (the updates of) twn-loops in our setting and analyze its complexity. Based on these results, we prove complexity bounds for the termination problem of twn-loops as well as tight bounds for two important classes of loops which can always be transformed into twn-loops. Finally, we show that there is an important class of linear loops. where our decision procedure results in an efficient procedure for termination analysis, i.e., where the parameterized complexity of deciding termination is polynomial.
      PubDate: 2023-12-04
       
  • Extending rely-guarantee thinking to handle real-time scheduling

    • Free pre-print version: Loading...

      Abstract: The reference point for developing any artefact is its specification; to develop software formally, a formal specification is required. For sequential programs, pre and post conditions (together with abstract objects) suffice; rely and guarantee conditions extend the scope of formal development approaches to tackle concurrency. In addition, real-time systems need ways of both requiring progress and relating that progress to some notion of time. This paper extends rely-guarantee ideas to cope with specifications of—and assumptions about—real-time schedulers. Furthermore it shows how the approach helps identify and specify fault-tolerance aspects of such schedulers by systematically challenging the assumptions.
      PubDate: 2023-11-30
       
  • Church synthesis on register automata over linearly ordered data domains

    • Free pre-print version: Loading...

      Abstract: In a Church synthesis game, two players, Adam and Eve, alternately pick some element in a finite alphabet, for an infinite number of rounds. The game is won by Eve if the \(\omega \) -word formed by this infinite interaction belongs to a given language S, called the specification. It is well-known that for \(\omega \) -regular specifications, it is decidable whether Eve has a strategy to enforce the specification no matter what Adam does. We study the extension of Church synthesis games to the linearly ordered data domains \(({\mathbb {Q}},\le )\) and \(({\mathbb {N}},\le )\) . In this setting, the infinite interaction between Adam and Eve results in an \(\omega \) -data word, i.e., an infinite sequence of elements in the domain. We study this problem when specifications are given as register automata. Those automata consist in finite automata equipped with a finite set of registers in which they can store data values, that they can then compare with incoming data values with respect to the linear order. Church games over \(({\mathbb {N}},\le )\) are however undecidable, even for deterministic register automata. Thus, we introduce one-sided Church games, where Eve instead operates over a finite alphabet, while Adam still manipulates data. We show that they are determined, and that deciding the existence of a winning strategy is in ExpTime, both for \({\mathbb {Q}}\) and \({\mathbb {N}}\) . This follows from a study of constraint sequences, which abstract the behaviour of register automata, and allow us to reduce Church games to \(\omega \) -regular games. We present an application of one-sided Church games to a transducer synthesis problem. In this application, a transducer models a reactive system (Eve) which outputs data stored in its registers, depending on its interaction with an environment (Adam) which inputs data to the system.
      PubDate: 2023-10-10
       
  • Thread-modular counter abstraction: automated safety and termination
           proofs of parameterized software by reduction to sequential program
           verification

    • Free pre-print version: Loading...

      Abstract: Parameterized programs are composed of an arbitrary number of concurrent, infinite-state threads. Automated safety and liveness proofs of such parameterized software are hard; state-of-the-art methods for their formal verification rely on intricate abstractions and complicated proof techniques that impede automation. In this paper, we introduce thread-modular counter abstraction (TMCA), a lean new abstraction technique to replace the existing heavy proof machinery. TMCA is a structured abstraction framework built from a novel combination of counter abstraction, thread-modular reasoning, and predicate abstraction. Its major strength lies in reducing the parameterized verification problem to the sequential setting, for which powerful proof procedures, efficient heuristics, and effective automated tools have been developed over the past decades. In this work, we first introduce the TMCA abstraction paradigm, then present a fully automated method for parameterized safety proofs, and finally discuss its application to automated termination and liveness proofs of parameterized software.
      PubDate: 2023-10-06
       
  • Enhancing active model learning with equivalence checking using simulation
           relations

    • Free pre-print version: Loading...

      Abstract: We present a new active model-learning approach to generating abstractions of a system from its execution traces. Given a system and a set of observables to collect execution traces, the abstraction produced by the algorithm is guaranteed to admit all system traces over the set of observables. To achieve this, the approach uses a pluggable model-learning component that can generate a model from a given set of traces. Conditions that encode a certain completeness hypothesis, formulated based on simulation relations, are then extracted from the abstraction under construction and used to evaluate its degree of completeness. The extracted conditions are sufficient to prove model completeness but not necessary. If all conditions are true, the algorithm terminates, returning a system overapproximation. A condition falsification may not necessarily correspond to missing system behaviour in the abstraction. This is resolved by applying model checking to determine whether it corresponds to any concrete system trace. If so, the new concrete trace is used to iteratively learn new abstractions, until all extracted completeness conditions are true. To evaluate the approach, we reverse-engineer a set of publicly available Simulink Stateflow models from their C implementations. Our algorithm generates an equivalent model for 98% of the Stateflow models.
      PubDate: 2023-08-06
      DOI: 10.1007/s10703-023-00433-y
       
  • Certified SAT solving with GPU accelerated inprocessing

    • Free pre-print version: Loading...

      Abstract: Abstract Since 2013, the leading SAT solvers in SAT competitions all use inprocessing, which, unlike preprocessing, interleaves search with simplifications. However, inprocessing is typically a performance bottleneck, in particular for hard or large formulas. In this work, we introduce the first attempt to parallelize inprocessing on GPU architectures. As one of the main challenges in GPU programming is memory locality, we present new compact data structures and devise a data-parallel garbage collector. It runs in parallel on the GPU to reduce memory consumption and improve memory locality. Our new parallel variable elimination algorithm is roughly twice as fast as previous work. Moreover, we augment the variable elimination with the first parallel algorithm for functional dependency extraction in an attempt to find more logical gates to eliminate that cannot be found with syntactic approaches. We present a novel algorithm to generate clausal proofs in parallel to validate all simplifications running on the GPU besides the CDCL search, giving high credibility to our solver and its use in critical applications such as model checkers. In experiments, our new solver ParaFROST solves numerous benchmarks faster on the GPU than its sequential counterparts. With functional dependency extraction, inprocessing in ParaFROST was more effective in reducing the solving time. Last but not least, all proofs generated by ParaFROST were successfully verified.
      PubDate: 2023-08-02
      DOI: 10.1007/s10703-023-00432-z
       
  • Dissecting ltlsynt

    • Free pre-print version: Loading...

      Abstract: Abstract ltlsynt is a tool for synthesizing a reactive circuit satisfying a specification expressed as an LTL formula. ltlsynt generally follows a textbook approach: the LTL specification is translated into a parity game whose winning strategy can be seen as a Mealy machine modeling a valid controller. This article details each step of this approach, and presents various refinements integrated over the years. Some of these refinements are unique to ltlsynt: for instance, ltlsynt supports multiple ways to encode a Mealy machine as an AIG circuit, features multiple simplification algorithms for the intermediate Mealy machine, and bypasses the usual game-theoretic approach for some subclasses of LTL formulas in favor of more direct constructions.
      PubDate: 2023-07-14
      DOI: 10.1007/s10703-022-00407-6
       
  • Round- and context-bounded control of dynamic pushdown systems

    • Free pre-print version: Loading...

      Abstract: Abstract We consider systems with unboundedly many processes that communicate through shared memory. In that context, simple verification questions have a high complexity or, in the case of pushdown processes, are even undecidable. Good algorithmic properties are recovered under round-bounded verification, which restricts the system behavior to a bounded number of round-robin schedules. In this paper, we extend this approach to a game-based setting. This allows one to solve synthesis and control problems and constitutes a further step towards a theory of languages over infinite alphabets.
      PubDate: 2023-07-07
      DOI: 10.1007/s10703-023-00431-0
       
  • Symbolic encoding of LL(1) parsing and its applications

    • Free pre-print version: Loading...

      Abstract: Abstract Parsers are omnipresent in almost all software systems. However, an operational implementation of parsers cannot answer many “how”, “why” and “what if” questions, why does this parser not accept this string, or, can we have to parser for it to accept a set of strings' To lift the parsing theory to answer such questions, we build a symbolic encoding of parsing. Our symbolic encoding, that we referred to as a parse condition, is a logical condition that is satisfiable if and only if a given string w can be successfully parsed using a grammar  \({\mathcal {G}}\) . We build an SMT encoding of such parse conditions for LL(1) grammars and demonstrate its utility by building three applications over it: automated repair of syntax errors in Tiger programs, automated parser synthesis to automatically synthesize LL(1) parsers from examples, and automatic root cause analysis of parser construction to debug errors in parse tables. We implement our ideas into a tool, Cyclops , that successfully repairs 80% of our benchmarks (675 buggy Tiger programs), clocking an average of 30 s per repair, synthesize parsers for interesting languages from examples, and ranks the ground truth as the topmost ranked reason for failure in more than 85% of our instances. On our deployment of Cyclops in a compiler design course, 91 of 128 students gave a positive response stating that assistance from Cyclops was indeed useful.
      PubDate: 2023-06-22
      DOI: 10.1007/s10703-023-00420-3
       
  • Memory access protocols: certified data-race freedom
           for GPU kernels

    • Free pre-print version: Loading...

      Abstract: Abstract GPUs offer parallelism as a commodity, but they are difficult to program correctly. Static analyzers that guarantee data-race freedom (DRF) are essential to help programmers establish the correctness of their programs (kernels). However, existing approaches produce too many false alarms and struggle to handle larger programs. To address these limitations we formalize a novel compositional analysis for DRF, based on memory access protocols. These protocols are behavioral types that codify the way threads interact over shared memory. Our work includes fully mechanized proofs of our theoretical results, the first mechanized proofs in the field of DRF analysis for GPU kernels. Our theory is implemented in Faial, a tool that outperforms the state-of-the-art. Notably, it can correctly verify at least \(1.42\times \) more real-world kernels, and it exhibits a linear growth in 4 out of 5 experiments, while others grow exponentially in all 5 experiments.
      PubDate: 2023-05-26
      DOI: 10.1007/s10703-023-00415-0
       
  • Compositional verification of priority systems using sharp bisimulation

    • Free pre-print version: Loading...

      Abstract: Abstract Sharp bisimulation is a refinement of branching bisimulation, parameterized by a subset of the system’s actions, called strong actions. This parameterization allows the sharp bisimulation to be tailored by the property under verification, whichever property of the modal \(\mu\) -calculus is considered, while potentially reducing more than strong bisimulation. Sharp bisimulation equivalence is a congruence for process algebraic operators such as parallel composition, hide, cut, and rename, and hence can be used in a compositional verification setting. In this paper, we prove that sharp bisimulation equivalence is also a congruence for action priority operators under some conditions on strong actions. We compare sharp bisimulation with orthogonal bisimulation, whose equivalence is also a congruence for action priority. We show that, if the internal action \(\tau\) neither gives priority to nor takes priority over other actions, then the quotient of a system with respect to sharp bisimulation equivalence (called sharp minimization) cannot be larger than the quotient of the same system with respect to orthogonal bisimulation equivalence. We then describe a signature-based partition refinement algorithm for sharp minimization, implemented in the BCG_MIN and BCG_CMP tools of the CADP software toolbox. This algorithm can be adapted to implement orthogonal minimization. We show on a crafted example that using compositional sharp minimization may yield state space reductions that outperform compositional orthogonal minimization by several orders of magnitude. Finally, we illustrate the use of sharp minimization and priority to verify a bully leader election algorithm.
      PubDate: 2023-05-17
      DOI: 10.1007/s10703-023-00422-1
       
  • Partial bounding for recursive function synthesis

    • Free pre-print version: Loading...

      Abstract: Abstract Quantifier bounding is a standard approach in inductive program synthesis to deal with unbounded domains. In this paper, we propose one such bounding method for the synthesis of recursive functions over recursive input data types. The synthesis problem is specified by an input reference (recursive) function and a recursion skeleton. The goal is to synthesize a recursive function equivalent to the input function whose recursion strategy is specified by the recursion skeleton. In this context, we illustrate that it is possible to selectively bound a subset of the recursively typed parameters, each by a suitable bound. The choices are guided by counterexamples. The evaluation of our strategy on a broad set of benchmarks shows that it succeeds in efficiently synthesizing non-trivial recursive functions where standard across-the-board bounding would fail.
      PubDate: 2023-05-16
      DOI: 10.1007/s10703-023-00417-y
       
  • Isla: integrating full-scale ISA semantics and axiomatic concurrency
           models (extended version)

    • Free pre-print version: Loading...

      Abstract: Abstract Architecture specifications such as Armv8-A and RISC-V are the ultimate foundation for software verification and the correctness criteria for hardware verification. They should define the allowed sequential and relaxed-memory concurrency behaviour of programs, but hitherto there has been no integration of full-scale instruction-set architecture (ISA) semantics with axiomatic concurrency models, either in mathematics or in tools. These ISA semantics can be surprisingly large and intricate, e.g. 100k \(+\) lines for Armv8-A. In this paper we present a tool, Isla, for computing the allowed behaviours of concurrent litmus tests with respect to full-scale ISA definitions, in the Sail language, and arbitrary axiomatic relaxed-memory concurrency models, in the Cat language. It is based on a generic symbolic engine for Sail ISA specifications. We equip the tool with a web interface to make it widely accessible, and illustrate and evaluate it for Armv8-A and RISC-V. The symbolic execution engine is valuable also for other verification tasks: it has been used in automated ISA test generation for the Arm Morello prototype architecture, extending Armv8-A with CHERI capabilities, and for Iris program-logic reasoning about binary code above the Armv8-A and RISC-V ISA specifications. By using full-scale and authoritative ISA semantics, Isla lets one evaluate litmus tests using arbitrary user instructions with high confidence. Moreover, because these ISA specifications give detailed and validated definitions of the sequential aspects of systems functionality, as used by hypervisors and operating systems, e.g. instruction fetch, exceptions, and address translation, our tool provides a basis for developing concurrency semantics for these. We demonstrate this for the Armv8-A instruction-fetch and virtual-memory models and examples of Simner et al.
      PubDate: 2023-05-12
      DOI: 10.1007/s10703-023-00409-y
       
  • Hashing-based approximate counting of minimal unsatisfiable subsets

    • Free pre-print version: Loading...

      Abstract: Abstract In many areas of computer science, we are given an unsatisfiable Boolean formula F in CNF, i.e. a set of clauses, with the goal to analyse the unsatisfiability. Examination of minimal unsatisfiable subsets (MUSes) of F is a kind of such analysis. While researchers in the past two decades focused mainly on techniques for explicit identification of MUSes, there have recently emerged various applications that do not require the explicit identification of MUSes. For instance, in the domain of diagnosis, it is often sufficient to count the number of MUSes. While in theory, one can simply count all MUSes by explicitly enumerating them, in practice, the complete explicit enumeration is often not possible for instances with a reasonably large number of MUSes. In this work, we describe our approximate MUS counting procedure called AMUSIC. Our approach avoids exhaustive MUS enumeration by combining the classical technique of universal hashing with advances in QBF solvers along with usage of union and intersection of MUSes to achieve runtime efficiency. Our prototype implementation of AMUSIC is shown to scale to instances that were clearly beyond the realm of enumeration-based approaches.
      PubDate: 2023-04-19
       
  • On multi-language abstraction: Towards a static analysis of multi-language
           programs

    • Free pre-print version: Loading...

      Abstract: Modern software development rarely takes place within a single programming language. Often, programmers appeal to cross-language interoperability. Examples are exploitation of novel features of one language within another, and cross-language code reuse. Our previous works developed a theory of so-called multi-languages, which arise by combining existing languages, defining a precise notion of (algebraic) multi-language semantics. As regards static analysis, the heterogeneity of the multi-language context opens up new and unexplored scenarios. In this paper, we provide a general theory for the combination of abstract interpretations of existing languages, regardless of their inherent nature, in order to gain an abstract semantics of multi-language programs. As a part of this general theory, we show that formal properties of interest of multi-language abstractions (e.g., soundness and completeness) boil down to the features of the interoperability mechanism that binds the underlying languages together. We extend many of the standard concepts of abstract interpretation to the framework of multi-languages.
      PubDate: 2023-03-28
       
  • Global guidance for local generalization in model checking

    • Free pre-print version: Loading...

      Abstract: Abstract SMT-based model checkers, especially IC3-style ones, are currently the most effective techniques for verification of infinite state systems. They infer global inductive invariants via local reasoning about a single step of the transition relation of a system, while employing SMT-based procedures, such as interpolation, to mitigate the limitations of local reasoning and allow for better generalization. Unfortunately, these mitigations intertwine model checking with heuristics of the underlying SMT-solver, negatively affecting stability of model checking. In this paper, we propose to tackle the limitations of locality in a systematic manner. We introduce explicit global guidance into the local reasoning performed by IC3-style algorithms. To this end, we extend the SMT-IC3 paradigm with three novel rules, designed to mitigate fundamental sources of failure that stem from locality. We instantiate these rules for Linear Integer Arithmetic and Linear Rational Aritmetic and implement them on top of Spacer solver in Z3. Our empirical results show that GSpacer, Spacer extended with global guidance, is significantly more effective than both Spacer and sole global reasoning, and, furthermore, is insensitive to interpolation.
      PubDate: 2023-03-28
       
  • Finite-trace and generalized-reactivity specifications in temporal
           synthesis

    • Free pre-print version: Loading...

      Abstract: Abstract Linear Temporal Logic (LTL) synthesis aims at automatically synthesizing a program that complies with desired properties expressed in LTL. Unfortunately it has been proved to be too difficult computationally to perform full LTL synthesis. There have been two success stories with LTL synthesis, both having to do with the form of the specification. The first is the GR(1) approach: use safety conditions to determine the possible transitions in a game between the environment and the agent, plus one powerful notion of fairness, Generalized Reactivity(1), or GR(1). The second, inspired by AI planning, is focusing on finite-trace temporal synthesis, with LTL \(_f\) (LTL on finite traces) as the specification language. In this paper we take these two lines of work and bring them together. We first study the case in which we have an LTL \(_f\) agent goal and a GR(1) environment specification. We then add to the framework safety conditions for both the environment and the agent, obtaining a highly expressive yet still scalable form of LTL synthesis.
      PubDate: 2023-03-15
       
  • Stochastic games with lexicographic objectives

    • Free pre-print version: Loading...

      Abstract: Abstract We study turn-based stochastic zero-sum games with lexicographic preferences over objectives. Stochastic games are standard models in control, verification, and synthesis of stochastic reactive systems that exhibit both randomness as well as controllable and adversarial non-determinism. Lexicographic order allows one to consider multiple objectives with a strict preference order. To the best of our knowledge, stochastic games with lexicographic objectives have not been studied before. For a mixture of reachability and safety objectives, we show that deterministic lexicographically optimal strategies exist and memory is only required to remember the already satisfied and violated objectives. For a constant number of objectives, we show that the relevant decision problem is in \(\textsf{NP}\cap \textsf{coNP}\) , matching the current known bound for single objectives; and in general the decision problem is \(\textsf{PSPACE}\) -hard and can be solved in \(\textsf{NEXPTIME}\cap \textsf{coNEXPTIME}\) . We present an algorithm that computes the lexicographically optimal strategies via a reduction to the computation of optimal strategies in a sequence of single-objectives games. For omega-regular objectives, we restrict our analysis to one-player games, also known as Markov decision processes. We show that lexicographically optimal strategies exist and need either randomization or finite memory. We present an algorithm that solves the relevant decision problem in polynomial time. We have implemented our algorithms and report experimental results on various case studies.
      PubDate: 2023-03-08
       
  • Stratified guarded first-order transition systems

    • Free pre-print version: Loading...

      Abstract: Abstract First-order transition systems are a convenient formalism to specify parametric systems such as multi-agent workflows or distributed algorithms. In general, any nontrivial question about such systems is undecidable. Here, we present three subclasses of first-order transition systems where every universal invariant can effectively be decided via fixpoint iteration. These subclasses are defined in terms of syntactical restrictions: negation, stratification and guardedness. While guardedness represents a particular pattern how input predicates control existential quantifiers, stratification limits the information flow between predicates. Guardedness implies that the weakest precondition for every universal invariant is again universal, while the remaining sufficient criteria enforce that either the number of occurring negated literals decreases in every iteration, or the number of required instances of input predicates or the number of first-order variables remains bounded. We argue for each of these three cases that termination of the fixpoint iteration can be guaranteed. We apply these results to identify classes of multi-agent systems, when formalized as first-order transition systems, where noninterference in presence of declassification is decidable for coalitions of attackers of bounded size.
      PubDate: 2022-11-22
       
  • Introducing robust reachability

    • Free pre-print version: Loading...

      Abstract: Abstract We introduce a new property called robust reachability which refines the standard notion of reachability in order to take replicability into account. A bug is robustly reachable if a controlled input can make it so the bug is reached whatever the value of uncontrolled input. Robust reachability is better suited than standard reachability in many realistic situations related to security (e.g., criticality assessment or bug prioritization) or software engineering (e.g., replicable test suites and flakiness). We propose a formal treatment of the concept, and we revisit existing symbolic bug finding methods through this new lens. Remarkably, robust reachability allows differentiating bounded model checking from symbolic execution while they have the same deductive power in the standard case. Finally, we propose the first symbolic verifier dedicated to robust reachability: we use it for criticality assessment of 5 existing vulnerabilities, and compare it with standard symbolic execution.
      PubDate: 2022-11-21
       
 
JournalTOCs
School of Mathematical and Computer Sciences
Heriot-Watt University
Edinburgh, EH14 4AS, UK
Email: journaltocs@hw.ac.uk
Tel: +00 44 (0)131 4513762
 


Your IP address: 18.205.26.39
 
Home (Search)
API
About JournalTOCs
News (blog, publications)
JournalTOCs on Twitter   JournalTOCs on Facebook

JournalTOCs © 2009-